- some additions and corrections

[helm.git] / matita / matita / contribs / lambda_delta / basic_2 / dynamic / snv_lift.ma

diff --git a/matita/matita/contribs/lambda_delta/basic_2/dynamic/snv_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/dynamic/snv_lift.ma
index 6d79ef571086474dc30eb177f1c0bb8684d5653a..67ab751c0e557a6a6a6ec447e24f7cd1c9060aa3 100644 (file)
--- a/matita/matita/contribs/lambda_delta/basic_2/dynamic/snv_lift.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/dynamic/snv_lift.ma
@@ -74,6 +74,6 @@ lemma snv_inv_lift: ∀h,g,L,U. ⦃h, L⦄ ⊩ U :[g] → ∀K,d,e. ⇩[d, e] L
 | #L #W0 #U #W #l #_ #_ #HUW #HW0 #IHW0 #IHU #K #d #e #HLK #X #H
   elim (lift_inv_flat2 … H) -H #V0 #T #HVW0 #HTU #H destruct
   elim (ssta_inv_lift1 … HUW … HLK … HTU) -HUW #V #HTV #HVW
-  lapply (cpcs_inv_lift … HLK … HVW … HVW0 ?) // -W /3 width=4/
+  lapply (cpcs_inv_lift … HLK … HVW0 … HVW ?) // -W /3 width=4/
 ]
 qed-.