#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 //