#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 //
qed-.
+
+(* Properties with iterated push ********************************************)
+
+lemma isid_pushs: ān,f. šā¦fā¦ ā šā¦ā*[n]fā¦.
+#n elim n -n /3 width=3 by isid_push/
+qed.
+
+(* Inversion lemmas with iterated push **************************************)
+
+lemma isid_inv_pushs: ān,g. šā¦ā*[n]gā¦ ā šā¦gā¦.
+#n elim n -n /3 width=3 by isid_inv_push/
+qed.
+
+(* Properties with tail *****************************************************)
+
+lemma isid_tl: āf. šā¦fā¦ ā šā¦ā«±fā¦.
+#f cases (pn_split f) * #g * -f #H
+[ /2 width=3 by isid_inv_push/
+| elim (isid_inv_next ā¦ H) -H //
+]
+qed.
+
+(* Properties with iterated tail ********************************************)
+
+lemma isid_tls: ān,g. šā¦gā¦ ā šā¦ā«±*[n]gā¦.
+#n elim n -n /3 width=1 by isid_tl/
+qed.