#j #Hg elim (at_inv_xnx ā¦ Hg ā¦ H) -Hg -H /2 width=2 by ex_intro/
qed-.
+(* Properties on tl *********************************************************)
+
+lemma istot_tl: āf. šā¦fā¦ ā šā¦āfā¦.
+#f cases (pn_split f) *
+#g * -f /2 width=3 by istot_inv_next, istot_inv_push/
+qed.
+
+(* Properties on minus ******************************************************)
+
+lemma istot_minus: ān,f. šā¦fā¦ ā šā¦f-nā¦.
+#n elim n -n /3 width=1 by istot_tl/
+qed.
+
(* Advanced forward lemmas on at ********************************************)
let corec at_ext: āf1,f2. šā¦f1ā¦ ā šā¦f2ā¦ ā