include "ground/relocation/gr_ist.ma".
include "ground/relocation/gr_after_pat.ma".
-(* RELATIONAL COMPOSITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* RELATIONAL COMPOSITION FOR GENERIC RELOCATION MAPS ***********************)
-(* Forward lemmas on istot **************************************************)
+(* Destructions with gr_ist *************************************************)
(*** after_istot_fwd *)
lemma gr_after_ist_des:
qed-.
(*** after_at1_fwd *)
-lemma gr_after_pat_sn_des:
+lemma gr_after_des_ist_pat:
∀f1,i1,i2. @❪i1, f1❫ ≘ i2 → ∀f2. 𝐓❪f2❫ → ∀f. f2 ⊚ f1 ≘ f →
∃∃i. @❪i2, f2❫ ≘ i & @❪i1, f❫ ≘ i.
#f1 #i1 #i2 #Hf1 #f2 #Hf2 #f #Hf elim (Hf2 i2) -Hf2
/3 width=8 by gr_after_des_pat, ex2_intro/
qed-.
-(* Inversions with gr_ist *)
+(* Inversions with gr_ist ***************************************************)
(*** after_inv_istot *)
lemma gr_after_inv_ist: