include "ground/relocation/gr_ist_isi.ma".
include "ground/relocation/gr_after_ist.ma".
-(* RELATIONAL COMPOSITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* RELATIONAL COMPOSITION FOR GENERIC RELOCATION MAPS ***********************)
-(* Forward lemmas on istot and isid **************************************************)
+(* Destructions with gr_ist and gr_isi **************************************)
(*** 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
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-.