(* Main inversion properties ************************************************)
theorem ist_inj: ān1,n2,c. šā¦n1,cā¦ ā šā¦n2,cā¦ ā n1 = n2.
(* Main inversion properties ************************************************)
theorem ist_inj: ān1,n2,c. šā¦n1,cā¦ ā šā¦n2,cā¦ ā n1 = n2.