X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fstatic%2Ffsle_drops.ma;h=718a74a8a8d578851090954d41f9885c12828304;hp=110e0fd08be6829db08f41239383fbc11e70aab9;hb=dc605ae41c39773f55381f241b1ed3db4acf5edd;hpb=caf822cbe34e204e6d1b72e272373b561c1a565a diff --git a/matita/matita/contribs/lambdadelta/static_2/static/fsle_drops.ma b/matita/matita/contribs/lambdadelta/static_2/static/fsle_drops.ma index 110e0fd08..718a74a8a 100644 --- a/matita/matita/contribs/lambdadelta/static_2/static/fsle_drops.ma +++ b/matita/matita/contribs/lambdadelta/static_2/static/fsle_drops.ma @@ -68,7 +68,7 @@ lemma fsle_inv_lifts_sn: ∀T1,U1. ⇧[1] T1 ≘ U1 → * #n #m #f2 #g2 #Hf2 #Hg2 #HL #Hfg2 #p elim (lveq_inv_pair_pair … HL) -HL #HL #H1 #H2 destruct elim (frees_total L2 V2) #g1 #Hg1 -elim (sor_isfin_ex g1 (⫱g2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #g #Hg #_ +elim (sor_isfin_ex g1 (⫰g2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #g #Hg #_ lapply (frees_inv_lifts_SO (Ⓣ) … Hf2 … HTU1) [1,2: /3 width=4 by drops_refl, drops_drop/ ] -U1 #Hf2 lapply (sor_inv_sle_dx … Hg) #H0g