(**************************************************************************)
include "ground_2/notation/relations/isidentity_1.ma".
-include "ground_2/relocation/rtmap_minus.ma".
+include "ground_2/relocation/rtmap_tls.ma".
(* RELOCATION MAP ***********************************************************)
#f #Hf * -g #g #H elim (discr_next_push ⦠H)
qed-.
-let corec isid_inv_eq_repl: āf1,f2. šā¦f1ā¦ ā šā¦f2⦠ā f1 ā f2 ā ?.
+(* Main inversion lemmas ****************************************************)
+
+corec theorem isid_inv_eq_repl: āf1,f2. šā¦f1ā¦ ā šā¦f2⦠ā f1 ā f2.
#f1 #f2 #H1 #H2
cases (isid_inv_gen ⦠H1) -H1
cases (isid_inv_gen ⦠H2) -H2
(* Basic properties *********************************************************)
-let corec isid_eq_repl_back: eq_repl_back ⦠isid ā ?.
+corec lemma isid_eq_repl_back: eq_repl_back ⦠isid.
#f1 #H cases (isid_inv_gen ⦠H) -H
#g1 #Hg1 #H1 #f2 #Hf cases (eq_inv_px ⦠Hf ⦠H1) -f1
/3 width=3 by isid_push/
(* Alternative definition ***************************************************)
-let corec eq_push_isid: āf. āf ā f ā šā¦f⦠ā ?.
+corec lemma eq_push_isid: āf. āf ā f ā šā¦fā¦.
#f #H cases (eq_inv_px ⦠H) -H /4 width=3 by isid_push, eq_trans/
qed.
-let corec eq_push_inv_isid: āf. šā¦f⦠ā āf ā f ā ?.
+corec lemma eq_push_inv_isid: āf. šā¦f⦠ā āf ā f.
#f * -f
#f #g #Hf #Hg @(eq_push ⦠Hg) [2: @eq_push_inv_isid // | skip ]
@eq_f //