#n #H destruct //
qed-.
+lemma ist_inv_10: ān. šā¦n,ššā¦ ā ā„.
+#h #H destruct
+qed-.
+
(* Main inversion properties ************************************************)
theorem ist_inj: ān1,n2,c. šā¦n1,cā¦ ā šā¦n2,cā¦ ā n1 = n2.