(* Basic inversion lemmas ***************************************************)
-lemma fcla_inv_px: â\88\80g,m. ð\9d\90\82â¦\83gâ¦\84 â\89¡ m â\86\92 â\88\80f. â\86\91f = g â\86\92 ð\9d\90\82â¦\83fâ¦\84 â\89¡ m.
+lemma fcla_inv_px: â\88\80g,m. ð\9d\90\82â¦\83gâ¦\84 â\89\98 m â\86\92 â\88\80f. â\86\91f = g â\86\92 ð\9d\90\82â¦\83fâ¦\84 â\89\98 m.
#g #m * -g -m /3 width=3 by fcla_isid, isid_inv_push/
#g #m #_ #f #H elim (discr_push_next … H)
qed-.
-lemma fcla_inv_nx: â\88\80g,m. ð\9d\90\82â¦\83gâ¦\84 â\89¡ m → ∀f. ⫯f = g →
- â\88\83â\88\83n. ð\9d\90\82â¦\83fâ¦\84 â\89¡ n & ⫯n = m.
+lemma fcla_inv_nx: â\88\80g,m. ð\9d\90\82â¦\83gâ¦\84 â\89\98 m → ∀f. ⫯f = g →
+ â\88\83â\88\83n. ð\9d\90\82â¦\83fâ¦\84 â\89\98 n & ⫯n = m.
#g #m * -g -m /2 width=3 by ex2_intro/
[ #g #Hg #f #H elim (isid_inv_next … H) -H //
| #g #m #_ #f #H elim (discr_next_push … H)
(* Advanced inversion lemmas ************************************************)
-lemma cla_inv_nn: â\88\80g,m. ð\9d\90\82â¦\83gâ¦\84 â\89¡ m â\86\92 â\88\80f,n. ⫯f = g â\86\92 ⫯n = m â\86\92 ð\9d\90\82â¦\83fâ¦\84 â\89¡ n.
+lemma cla_inv_nn: â\88\80g,m. ð\9d\90\82â¦\83gâ¦\84 â\89\98 m â\86\92 â\88\80f,n. ⫯f = g â\86\92 ⫯n = m â\86\92 ð\9d\90\82â¦\83fâ¦\84 â\89\98 n.
#g #m #H #f #n #H1 #H2 elim (fcla_inv_nx … H … H1) -g
#x #Hf #H destruct //
qed-.
-lemma cla_inv_np: â\88\80g,m. ð\9d\90\82â¦\83gâ¦\84 â\89¡ m → ∀f. ⫯f = g → 0 = m → ⊥.
+lemma cla_inv_np: â\88\80g,m. ð\9d\90\82â¦\83gâ¦\84 â\89\98 m → ∀f. ⫯f = g → 0 = m → ⊥.
#g #m #H #f #H1 elim (fcla_inv_nx … H … H1) -g
#x #_ #H1 #H2 destruct
qed-.
-lemma fcla_inv_xp: â\88\80g,m. ð\9d\90\82â¦\83gâ¦\84 â\89¡ m → 0 = m → 𝐈⦃g⦄.
+lemma fcla_inv_xp: â\88\80g,m. ð\9d\90\82â¦\83gâ¦\84 â\89\98 m → 0 = m → 𝐈⦃g⦄.
#g #m #H elim H -g -m /3 width=3 by isid_push/
#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: â\88\80n. eq_repl_back â\80¦ (λf. ð\9d\90\82â¦\83fâ¦\84 â\89¡ n).
+lemma fcla_eq_repl_back: â\88\80n. eq_repl_back â\80¦ (λf. ð\9d\90\82â¦\83fâ¦\84 â\89\98 n).
#n #f1 #H elim H -f1 -n /3 width=3 by fcla_isid, isid_eq_repl_back/
#f1 #n #_ #IH #g2 #H [ elim (eq_inv_px … H) | elim (eq_inv_nx … H) ] -H
/3 width=3 by fcla_push, fcla_next/
qed-.
-lemma fcla_eq_repl_fwd: â\88\80n. eq_repl_fwd â\80¦ (λf. ð\9d\90\82â¦\83fâ¦\84 â\89¡ n).
+lemma fcla_eq_repl_fwd: â\88\80n. eq_repl_fwd â\80¦ (λf. ð\9d\90\82â¦\83fâ¦\84 â\89\98 n).
#n @eq_repl_sym /2 width=3 by fcla_eq_repl_back/
qed-.