(*** fcla *)
inductive pr_fcla: relation2 pr_map nat ≝
(*** fcla_isid *)
-| pr_fcla_isi (f): ð\9d\90\88â\9dªfâ\9d« → pr_fcla f (𝟎)
+| pr_fcla_isi (f): ð\9d\90\88â\9d¨fâ\9d© → pr_fcla f (𝟎)
(*** fcla_push *)
| pr_fcla_push (f) (n): pr_fcla f n → pr_fcla (⫯f) n
(*** fcla_next *)
(* Basic inversions *********************************************************)
(*** fcla_inv_px *)
-lemma pr_fcla_inv_push (g) (m): ð\9d\90\82â\9dªgâ\9d« â\89\98 m â\86\92 â\88\80f. ⫯f = g â\86\92 ð\9d\90\82â\9dªfâ\9d« ≘ m.
+lemma pr_fcla_inv_push (g) (m): ð\9d\90\82â\9d¨gâ\9d© â\89\98 m â\86\92 â\88\80f. ⫯f = g â\86\92 ð\9d\90\82â\9d¨fâ\9d© ≘ m.
#g #m * -g -m
[ /3 width=3 by pr_fcla_isi, pr_isi_inv_push/
| #g #m #Hg #f #H >(eq_inv_pr_push_bi … H) -f //
qed-.
(*** fcla_inv_nx *)
-lemma pr_fcla_inv_next (g) (m): ð\9d\90\82â\9dªgâ\9d« â\89\98 m â\86\92 â\88\80f. â\86\91f = g â\86\92 â\88\83â\88\83n. ð\9d\90\82â\9dªfâ\9d« ≘ n & ↑n = m.
+lemma pr_fcla_inv_next (g) (m): ð\9d\90\82â\9d¨gâ\9d© â\89\98 m â\86\92 â\88\80f. â\86\91f = g â\86\92 â\88\83â\88\83n. ð\9d\90\82â\9d¨fâ\9d© ≘ n & ↑n = m.
#g #m * -g -m
[ #g #Hg #f #H destruct
elim (pr_isi_inv_next … Hg) -Hg //
(* Advanced inversions ******************************************************)
(*** cla_inv_nn *)
-lemma pr_cla_inv_next_succ (g) (m): ð\9d\90\82â\9dªgâ\9d« â\89\98 m â\86\92 â\88\80f,n. â\86\91f = g â\86\92 â\86\91n = m â\86\92 ð\9d\90\82â\9dªfâ\9d« ≘ n.
+lemma pr_cla_inv_next_succ (g) (m): ð\9d\90\82â\9d¨gâ\9d© â\89\98 m â\86\92 â\88\80f,n. â\86\91f = g â\86\92 â\86\91n = m â\86\92 ð\9d\90\82â\9d¨fâ\9d© ≘ n.
#g #m #H #f #n #H1 #H2 elim (pr_fcla_inv_next … H … H1) -g
#x #Hf #H destruct <(eq_inv_nsucc_bi … H) -n //
qed-.
(*** cla_inv_np *)
-lemma pr_cla_inv_next_zero (g) (m): ð\9d\90\82â\9dªgâ\9d« ≘ m → ∀f. ↑f = g → 𝟎 = m → ⊥.
+lemma pr_cla_inv_next_zero (g) (m): ð\9d\90\82â\9d¨gâ\9d© ≘ m → ∀f. ↑f = g → 𝟎 = m → ⊥.
#g #m #H #f #H1 elim (pr_fcla_inv_next … H … H1) -g
#x #_ #H1 #H2 destruct /2 width=2 by eq_inv_zero_nsucc/
qed-.
(*** fcla_inv_xp *)
-lemma pr_fcla_inv_zero (g) (m): ð\9d\90\82â\9dªgâ\9d« â\89\98 m â\86\92 ð\9d\9f\8e = m â\86\92 ð\9d\90\88â\9dªgâ\9d«.
+lemma pr_fcla_inv_zero (g) (m): ð\9d\90\82â\9d¨gâ\9d© â\89\98 m â\86\92 ð\9d\9f\8e = m â\86\92 ð\9d\90\88â\9d¨gâ\9d©.
#g #m #H elim H -g -m /3 width=3 by pr_isi_push/
#g #m #_ #_ #H destruct elim (eq_inv_zero_nsucc … H)
qed-.
(*** fcla_inv_isid *)
-lemma pr_fcla_inv_isi (g) (m): ð\9d\90\82â\9dªgâ\9d« â\89\98 m â\86\92 ð\9d\90\88â\9dªgâ\9d« → 𝟎 = m.
+lemma pr_fcla_inv_isi (g) (m): ð\9d\90\82â\9d¨gâ\9d© â\89\98 m â\86\92 ð\9d\90\88â\9d¨gâ\9d© → 𝟎 = m.
#f #n #H elim H -f -n /3 width=3 by pr_isi_inv_push/
#f #n #_ #_ #H elim (pr_isi_inv_next … H) -H //
qed-.