λδ-2B is released

[helm.git] / matita / matita / contribs / lambdadelta / static_2 / relocation / lifts_teqo.ma

diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_teqo.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_teqo.ma
index be94378433006db33182e900570d67ec2b752c22..0a6831c7211bc81078c195c651cc6adbb9842102 100644 (file)
--- a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_teqo.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_teqo.ma
@@ -21,7 +21,7 @@ include "static_2/relocation/lifts_lifts.ma".
 
 lemma teqo_lifts_sn: liftable2_sn teqo.
 #T1 #T2 #H elim H -T1 -T2 [||| * ]
-[ #s1 #s2 #f #X #H 
+[ #s1 #s2 #f #X #H
   >(lifts_inv_sort1 … H) -H
   /2 width=3 by teqo_sort, ex2_intro/
 | #i #f #X #H