X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Frelocation%2Fgr_after_ist_isi.ma;h=fd325b4d73a6b5eab930c882316b5564231b9d32;hp=93077d253e3544e23831141ced1c4ee7cd8ad411;hb=0bcf2dc1a27e38cb6cd3d44eb838d652926841e0;hpb=7e120a2bf2e6c0882b4f4b376c5861e001945cf4

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_ist_isi.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_ist_isi.ma
index 93077d253..fd325b4d7 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_ist_isi.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_ist_isi.ma
@@ -20,7 +20,7 @@ include "ground/relocation/gr_after_ist.ma".
 (* Forward lemmas on istot and isid **************************************************)
 
 (*** after_fwd_isid_sn *)
-lemma gr_after_des_isi_sn:
+lemma gr_after_des_ist_eq_sn:
       ∀f2,f1,f. 𝐓❪f❫ → f2 ⊚ f1 ≘ f → f1 ≡ f → 𝐈❪f2❫.
 #f2 #f1 #f #H #Hf elim (gr_after_inv_ist … Hf H) -H
 #Hf2 #Hf1 #H @gr_isi_pat_total // -Hf2
@@ -31,10 +31,10 @@ lemma gr_after_des_isi_sn:
 qed-.
 
 (*** after_fwd_isid_dx *)
-lemma gr_after_des_isi_dx:
+lemma gr_after_des_ist_eq_dx:
       ∀f2,f1,f.  𝐓❪f❫ → f2 ⊚ f1 ≘ f → f2 ≡ f → 𝐈❪f1❫.
 #f2 #f1 #f #H #Hf elim (gr_after_inv_ist … Hf H) -H
 #Hf2 #Hf1 #H2 @gr_isi_pat_total // -Hf1
-#i1 #i2 #Hi12 elim (gr_after_pat_sn_des … Hi12 … Hf) -f1
+#i1 #i2 #Hi12 elim (gr_after_des_ist_pat … Hi12 … Hf) -f1
 /3 width=8 by gr_pat_inj, gr_pat_eq_repl_back/
 qed-.