X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_transition%2Flfpx.ma;h=0fc26a744b702380be2bb6805a4138cbab4c8b85;hb=5224d5d0ff327a2360c9acd282af66ceed8788fc;hp=ad9f1e03fa40f3b6ea091022b62b6dfd6bc538e8;hpb=5e5f9111df82a2f84f2b560ab59392cf0e0906c0;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx.ma
index ad9f1e03f..0fc26a744 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx.ma
@@ -54,10 +54,10 @@ lemma lfpx_pair_repl_dx: ∀h,I,G,L1,L2,T,V,V1.
 
 (* Basic inversion lemmas ***************************************************)
 
-lemma lfpx_inv_atom_sn: ∀h,I,G,Y2. ⦃G, ⋆⦄ ⊢ ⬈[h, ⓪{I}] Y2 → Y2 = ⋆.
+lemma lfpx_inv_atom_sn: ∀h,G,Y2,T. ⦃G, ⋆⦄ ⊢ ⬈[h, T] Y2 → Y2 = ⋆.
 /2 width=3 by lfxs_inv_atom_sn/ qed-.
 
-lemma lfpx_inv_atom_dx: ∀h,I,G,Y1. ⦃G, Y1⦄ ⊢ ⬈[h, ⓪{I}] ⋆ → Y1 = ⋆.
+lemma lfpx_inv_atom_dx: ∀h,G,Y1,T. ⦃G, Y1⦄ ⊢ ⬈[h, T] ⋆ → Y1 = ⋆.
 /2 width=3 by lfxs_inv_atom_dx/ qed-.
 
 lemma lfpx_inv_sort: ∀h,G,Y1,Y2,s. ⦃G, Y1⦄ ⊢ ⬈[h, ⋆s] Y2 →