Changeset 352 for Deliverables/D4.1/Matita/Vector.ma
 Timestamp:
 Dec 1, 2010, 6:03:45 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Vector.ma
r350 r352 139 139 match split A m' n (tl⌈Vector A (m'+n)↦Vector A o⌉) with 140 140 [ mk_Cartesian v1 v2 ⇒ 〈he:::v1, v2〉 ]] (?: (S (m' + n)) = S (m' + n))]. 141 // ; ndestruct; //.141 // [ ndestruct  nlapply (S_inj … K); //] 142 142 nqed. 143 143 … … 148 148  Cons o he tl ⇒ λK. 〈he,(tl⌈Vector A n ↦ Vector A o⌉)〉 149 149 ] (? : S ? = S ?). 150 // ; ndestruct; //.150 // [ ndestruct  nlapply (S_inj … K); //] 151 151 nqed. 152 152 … … 181 181 ] 182 182 ]) (refl ? n). 183 ndestruct; //. 183 ##[##1,2: ndestruct  ##3,4: nlapply (S_inj … prf); // ] 184 184 nqed. 185 185 … … 219 219 ndestruct(e); 220 220 ## 221  n destruct(e);221  nlapply (S_inj … e); #H; nrewrite > H; 222 222 napply tl' 223 223 ## … … 397 397 ] 398 398 ]) (refl ? n). 399 ##[##1, 3: 400 ndestruct (absd); 401 ndestruct (prf); 402 napply tl'; 403 ####2: 404 ndestruct (absd); 405 ##] 399 ##[##1,2: ndestruct 400  nlapply (S_inj … prf); #X; nrewrite < X; 401 napply tl' ] 406 402 nqed. 407 403
Note: See TracChangeset
for help on using the changeset viewer.