#g #m #_ #_ #H destruct
qed-.
+lemma fcla_inv_isid: āf,n. šā¦fā¦ ā” n ā šā¦fā¦ ā 0 = n.
+#f #n #H elim H -f -n /3 width=3 by isid_inv_push/
+#f #n #_ #_ #H elim (isid_inv_next ā¦ H) -H //
+qed-.
+
+(* Main forward lemmas ******************************************************)
+
+theorem fcla_mono: āf,n1. šā¦fā¦ ā” n1 ā ān2. šā¦fā¦ ā” n2 ā n1 = n2.
+#f #n #H elim H -f -n
+[ /2 width=3 by fcla_inv_isid/
+| /3 width=3 by fcla_inv_px/
+| #f #n1 #_ #IH #n2 #H elim (fcla_inv_nx ā¦ H) -H [2,3 : // ]
+ #g #Hf #H destruct /3 width=1 by eq_f/
+]
+qed-.
+
(* Basic properties *********************************************************)
lemma fcla_eq_repl_back: ān. eq_repl_back ā¦ (Ī»f. šā¦fā¦ ā” n).