inductive fcla: relation2 rtmap nat ≝
| fcla_isid: ∀f. 𝐈⦃f⦄ → fcla f 0
-| fcla_push: â\88\80f,n. fcla f n â\86\92 fcla (â\86\91f) n
-| fcla_next: â\88\80f,n. fcla f n â\86\92 fcla (⫯f) (⫯n)
+| fcla_push: â\88\80f,n. fcla f n â\86\92 fcla (⫯f) n
+| fcla_next: â\88\80f,n. fcla f n â\86\92 fcla (â\86\91f) (â\86\91n)
.
interpretation "finite colength assignment (rtmap)"
(* Basic inversion lemmas ***************************************************)
-lemma fcla_inv_px: â\88\80g,m. ð\9d\90\82â¦\83gâ¦\84 â\89\98 m â\86\92 â\88\80f. â\86\91f = g → 𝐂⦃f⦄ ≘ m.
+lemma fcla_inv_px: â\88\80g,m. ð\9d\90\82â¦\83gâ¦\84 â\89\98 m â\86\92 â\88\80f. ⫯f = g → 𝐂⦃f⦄ ≘ 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\98 m â\86\92 â\88\80f. ⫯f = g →
- â\88\83â\88\83n. ð\9d\90\82â¦\83fâ¦\84 â\89\98 n & ⫯n = m.
+lemma fcla_inv_nx: â\88\80g,m. ð\9d\90\82â¦\83gâ¦\84 â\89\98 m â\86\92 â\88\80f. â\86\91f = g →
+ â\88\83â\88\83n. ð\9d\90\82â¦\83fâ¦\84 â\89\98 n & â\86\91n = 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\98 m â\86\92 â\88\80f,n. ⫯f = g â\86\92 ⫯n = m → 𝐂⦃f⦄ ≘ n.
+lemma cla_inv_nn: â\88\80g,m. ð\9d\90\82â¦\83gâ¦\84 â\89\98 m â\86\92 â\88\80f,n. â\86\91f = g â\86\92 â\86\91n = m → 𝐂⦃f⦄ ≘ 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\98 m â\86\92 â\88\80f. ⫯f = g → 0 = m → ⊥.
+lemma cla_inv_np: â\88\80g,m. ð\9d\90\82â¦\83gâ¦\84 â\89\98 m â\86\92 â\88\80f. â\86\91f = g → 0 = m → ⊥.
#g #m #H #f #H1 elim (fcla_inv_nx … H … H1) -g
#x #_ #H1 #H2 destruct
qed-.