Convert subsingleton

Signed-off-by: zeramorphic <[email protected]>

ConNF/BaseType/NearLitter.lean

@@ -281,7 +281,6 @@ theorem NearLitter.inter_nonempty_of_fst_eq_fst {N₁ N₂ : NearLitter} (h : N
   rw [← nonempty_coe_sort, ← mk_ne_zero_iff, mk_inter_of_fst_eq_fst h]
   exact mk_ne_zero κ
 
-
 theorem NearLitter.inter_small_of_fst_ne_fst {N₁ N₂ : NearLitter} (h : N₁.fst ≠ N₂.fst) :
     Small (N₁ ∩ N₂ : Set Atom) := by
   have := N₁.2.2

ConNF/Counting/Spec.lean

@@ -20,8 +20,8 @@ inductive SpecCondition (β : Λ)
   | atom (A : ExtendedIndex β) (s : Set κ) (t : Set κ)
   | flexible (A : ExtendedIndex β) (s : Set κ)
   | inflexibleCoe (A : ExtendedIndex β) (h : InflexibleCoePath A)
-      (χ : CodingFunction h.δ) (hχ : χ.Strong)
-  | inflexibleBot (A : ExtendedIndex β) (h : InflexibleBotPath A) (s : Set κ)
+      (χ : CodingFunction h.δ) (hχ : χ.Strong) (t : κ → Set κ)
+  | inflexibleBot (A : ExtendedIndex β) (h : InflexibleBotPath A) (s : Set κ) (t : κ → Set κ)
 
 abbrev Spec (β : Λ) := Enumeration (SpecCondition β)
 
@@ -61,11 +61,78 @@ structure Specifies (σ : Spec β) (S : Support β) (hS : S.Strong) : Prop where
           (before_comp_supports S hS hi h hSi))
         (CodingFunction.code_strong _ _ _
           (Support.comp_strong _ _ (Support.before_strong _ _ _ hS)))
+        (fun j => {k | ∃ hj hk, ∃ (a : Atom) (N' : NearLitter),
+          N'.1 = N.1 ∧ a ∈ (N : Set Atom) ∆ N' ∧
+          S.f j hj = ⟨A, inr N'⟩ ∧ S.f k hk = ⟨A, inl a⟩})
   inflexibleBot_spec (i : κ) (hi : i < S.max) (A : ExtendedIndex β) (N : NearLitter)
       (h : InflexibleBot A N.1) :
       S.f i hi = ⟨A, inr N⟩ →
       σ.f i (hi.trans_eq max_eq_max) = SpecCondition.inflexibleBot A h.path
         {j | ∃ hj, S.f j hj = ⟨h.path.B.cons (bot_lt_coe _), inl h.a⟩}
+        (fun j => {k | ∃ hj hk, ∃ (a : Atom) (N' : NearLitter),
+            N'.1 = N.1 ∧ a ∈ (N : Set Atom) ∆ N' ∧
+            S.f j hj = ⟨A, inr N'⟩ ∧ S.f k hk = ⟨A, inl a⟩})
+
+theorem Specifies.of_eq_atom {σ : Spec β} {S : Support β} {hS : S.Strong} (h : σ.Specifies S hS)
+    {i : κ} {hi : i < σ.max} {A : ExtendedIndex β} {s t : Set κ}
+    (hi' : σ.f i hi = SpecCondition.atom A s t) :
+    ∃ a, S.f i (hi.trans_eq h.max_eq_max.symm) = ⟨A, inl a⟩ := by
+  have hiS := hi.trans_eq h.max_eq_max.symm
+  set c := S.f i hiS with hc
+  obtain ⟨B, a | N⟩ := c
+  · cases hi'.symm.trans (h.atom_spec i hiS B a hc.symm)
+    exact ⟨a, rfl⟩
+  obtain (hN | ⟨⟨hN⟩⟩ | ⟨⟨hN⟩⟩) := flexible_cases' B N.1
+  · cases hi'.symm.trans (h.flexible_spec i hiS B N hN hc.symm)
+  · cases hi'.symm.trans (h.inflexibleBot_spec i hiS B N hN hc.symm)
+  · cases hi'.symm.trans (h.inflexibleCoe_spec i hiS B N hN hc.symm)
+
+theorem Specifies.of_eq_flexible {σ : Spec β} {S : Support β} {hS : S.Strong} (h : σ.Specifies S hS)
+    {i : κ} {hi : i < σ.max} {A : ExtendedIndex β} {s : Set κ}
+    (hi' : σ.f i hi = SpecCondition.flexible A s) :
+    ∃ N, Flexible A N.1 ∧ S.f i (hi.trans_eq h.max_eq_max.symm) = ⟨A, inr N⟩ := by
+  have hiS := hi.trans_eq h.max_eq_max.symm
+  set c := S.f i hiS with hc
+  obtain ⟨B, a | N⟩ := c
+  · cases hi'.symm.trans (h.atom_spec i hiS B a hc.symm)
+  obtain (hN | ⟨⟨hN⟩⟩ | ⟨⟨hN⟩⟩) := flexible_cases' B N.1
+  · cases hi'.symm.trans (h.flexible_spec i hiS B N hN hc.symm)
+    exact ⟨N, hN, rfl⟩
+  · cases hi'.symm.trans (h.inflexibleBot_spec i hiS B N hN hc.symm)
+  · cases hi'.symm.trans (h.inflexibleCoe_spec i hiS B N hN hc.symm)
+
+theorem Specifies.of_eq_inflexibleCoe {σ : Spec β} {S : Support β} {hS : S.Strong}
+    (h : σ.Specifies S hS)
+    {i : κ} {hi : i < σ.max} {A : ExtendedIndex β} {P : InflexibleCoePath A}
+    {χ : CodingFunction P.δ} {hχ : χ.Strong} {s : κ → Set κ}
+    (hi' : σ.f i hi = SpecCondition.inflexibleCoe A P χ hχ s) :
+    ∃ N t, N.1 = fuzz P.hδε t ∧ S.f i (hi.trans_eq h.max_eq_max.symm) = ⟨A, inr N⟩ := by
+  have hiS := hi.trans_eq h.max_eq_max.symm
+  set c := S.f i hiS with hc
+  obtain ⟨B, a | N⟩ := c
+  · cases hi'.symm.trans (h.atom_spec i hiS B a hc.symm)
+  obtain (hN | ⟨⟨hN⟩⟩ | ⟨⟨hN⟩⟩) := flexible_cases' B N.1
+  · cases hi'.symm.trans (h.flexible_spec i hiS B N hN hc.symm)
+  · cases hi'.symm.trans (h.inflexibleBot_spec i hiS B N hN hc.symm)
+  · cases hi'.symm.trans (h.inflexibleCoe_spec i hiS B N hN hc.symm)
+    exact ⟨N, hN.t, hN.hL, rfl⟩
+
+theorem Specifies.of_eq_inflexibleBot {σ : Spec β} {S : Support β} {hS : S.Strong}
+    (h : σ.Specifies S hS)
+    {i : κ} {hi : i < σ.max} {A : ExtendedIndex β} {P : InflexibleBotPath A}
+    {s : Set κ} {t : κ → Set κ}
+    (hi' : σ.f i hi = SpecCondition.inflexibleBot A P s t) :
+    ∃ N a, N.1 = fuzz (bot_ne_coe (a := P.ε)) a ∧
+      S.f i (hi.trans_eq h.max_eq_max.symm) = ⟨A, inr N⟩ := by
+  have hiS := hi.trans_eq h.max_eq_max.symm
+  set c := S.f i hiS with hc
+  obtain ⟨B, a | N⟩ := c
+  · cases hi'.symm.trans (h.atom_spec i hiS B a hc.symm)
+  obtain (hN | ⟨⟨hN⟩⟩ | ⟨⟨hN⟩⟩) := flexible_cases' B N.1
+  · cases hi'.symm.trans (h.flexible_spec i hiS B N hN hc.symm)
+  · cases hi'.symm.trans (h.inflexibleBot_spec i hiS B N hN hc.symm)
+    exact ⟨N, hN.a, hN.hL, rfl⟩
+  · cases hi'.symm.trans (h.inflexibleCoe_spec i hiS B N hN hc.symm)
 
 end Spec
 

ConNF/Counting/SpecSame.lean

@@ -7,6 +7,8 @@ import ConNF.Counting.Spec
 
 open Quiver Set Sum WithBot
 
+open scoped symmDiff
+
 universe u
 
 namespace ConNF
@@ -87,29 +89,165 @@ theorem convert_inflexibleCoe {A : ExtendedIndex β} {NS NT : NearLitter} (P : I
     cases this.1
     exact ⟨t', hNT⟩
 
+theorem convert_inflexibleBot {A : ExtendedIndex β} {NS NT : NearLitter} (P : InflexibleBotPath A)
+    (a : Atom) (hNS : NS.1 = fuzz (bot_ne_coe (a := P.ε)) a)
+    {i : κ} (hiS : i < S.max) (hiT : i < T.max)
+    (hiNS : S.f i hiS = ⟨A, inr NS⟩) (hiNT : T.f i hiT = ⟨A, inr NT⟩) :
+    ∃ (a' : Atom), NT.1 = fuzz (bot_ne_coe (a := P.ε)) a' := by
+  obtain (hN | ⟨⟨P', a', hNT⟩⟩ | ⟨⟨hN⟩⟩) := flexible_cases' A NT.1
+  · have h₁ := hσS.inflexibleBot_spec i hiS A NS ⟨P, a, hNS⟩ hiNS
+    have h₂ := hσT.flexible_spec i hiT A NT hN hiNT
+    cases h₁.symm.trans h₂
+  · have h₁ := hσS.inflexibleBot_spec i hiS A NS ⟨P, a, hNS⟩ hiNS
+    have h₂ := hσT.inflexibleBot_spec i hiT A NT ⟨P', a', hNT⟩ hiNT
+    have := h₁.symm.trans h₂
+    simp only [SpecCondition.inflexibleBot.injEq, heq_eq_eq, true_and] at this
+    cases this.1
+    exact ⟨a', hNT⟩
+  · have h₁ := hσS.inflexibleBot_spec i hiS A NS ⟨P, a, hNS⟩ hiNS
+    have h₂ := hσT.inflexibleCoe_spec i hiT A NT hN hiNT
+    cases h₁.symm.trans h₂
+
+theorem comp_eq_same {i : κ} (hiS : i < S.max) {γ : Λ} (A : Path (β : TypeIndex) γ)
+    (c : Address γ) (hc : S.f i hiS = ⟨A.comp c.1, c.2⟩) :
+    ∃ d : Address γ, T.f i (hiS.trans_eq (hσS.max_eq_max.trans hσT.max_eq_max.symm)) =
+      ⟨A.comp d.1, d.2⟩ := by
+  obtain ⟨B, a | N⟩ := c
+  · have := hσS.atom_spec i hiS (A.comp B) a hc
+    obtain ⟨a', ha'⟩ := hσT.of_eq_atom this
+    exact ⟨⟨B, inl a'⟩, ha'⟩
+  obtain (hN | ⟨⟨hN⟩⟩ | ⟨⟨hN⟩⟩) := flexible_cases' (A.comp B) N.1
+  · have := hσS.flexible_spec i hiS (A.comp B) N hN hc
+    obtain ⟨N', -, hN'₂⟩ := hσT.of_eq_flexible this
+    exact ⟨⟨B, inr N'⟩, hN'₂⟩
+  · have := hσS.inflexibleBot_spec i hiS (A.comp B) N hN hc
+    obtain ⟨N', hN'₁, -, hN'₃⟩ := hσT.of_eq_inflexibleBot this
+    exact ⟨⟨B, inr N'⟩, hN'₃⟩
+  · have := hσS.inflexibleCoe_spec i hiS (A.comp B) N hN hc
+    obtain ⟨N', hN'₁, -, hN'₃⟩ := hσT.of_eq_inflexibleCoe this
+    exact ⟨⟨B, inr N'⟩, hN'₃⟩
+
+theorem convertNearLitter_subsingleton_inflexibleCoe (A : ExtendedIndex β) (NS NT NT' : NearLitter)
+    (h : ConvertNearLitter S T A NS NT) (h' : ConvertNearLitter S T A NS NT')
+    (hNS : InflexibleCoe A NS.1) : NT = NT' := by
+  obtain ⟨P, t, hNS⟩ := hNS
+  obtain ⟨i, hiS₁, hiT₁, hiS₂, hiT₂⟩ := h
+  obtain ⟨i', hiS₁', hiT₁', hiS₂', hiT₂'⟩ := h'
+  have h₁ := hσS.inflexibleCoe_spec i hiS₁ A NS ⟨P, t, hNS⟩ hiS₂
+  have h₂ := hσS.inflexibleCoe_spec i' hiS₁' A NS ⟨P, t, hNS⟩ hiS₂'
+  obtain ⟨u, hNT⟩ := convert_inflexibleCoe hσS hσT P t hNS hiS₁ hiT₁ hiS₂ hiT₂
+  obtain ⟨u', hNT'⟩ := convert_inflexibleCoe hσS hσT P t hNS hiS₁' hiT₁' hiS₂' hiT₂'
+  have h₃ := hσT.inflexibleCoe_spec i hiT₁ A NT ⟨P, u, hNT⟩ hiT₂
+  have h₄ := hσT.inflexibleCoe_spec i' hiT₁' A NT' ⟨P, u', hNT'⟩ hiT₂'
+  have h₅ := h₁.symm.trans h₃
+  have h₆ := h₂.symm.trans h₄
+  clear h₁ h₂ h₃ h₄
+  simp only [SpecCondition.inflexibleCoe.injEq, heq_eq_eq, CodingFunction.code_eq_code_iff,
+    true_and] at h₅ h₆
+  obtain ⟨⟨ρ, h₅, rfl⟩, h₅'⟩ := h₅
+  obtain ⟨⟨ρ', h₆, rfl⟩, -⟩ := h₆
+  have : ρ • t = ρ' • t
+  · clear h₅'
+    have := support_supports t (ρ'⁻¹ * ρ) ?_
+    · conv_rhs => rw [← this]
+      rw [mul_smul, smul_smul, mul_right_inv, one_smul]
+    intro c hc
+    rw [mul_smul, inv_smul_eq_iff]
+    have : ∃ (j : κ) (hj : j < S.max), j < i ∧ j < i' ∧ S.f j hj = ⟨(P.B.cons P.hδ).comp c.1, c.2⟩
+    · by_cases hii' : i < i'
+      · have h₇ := Support.Precedes.fuzz A NS ⟨P, t, hNS⟩ _ hc
+        rw [← P.hA, ← hiS₂] at h₇
+        obtain ⟨j, hj, hji, hjc⟩ := hS.precedes hiS₁ _ h₇
+        exact ⟨j, hj, hji, hji.trans hii', hjc⟩
+      · have h₇ := Support.Precedes.fuzz A NS ⟨P, t, hNS⟩ _ hc
+        rw [← P.hA, ← hiS₂'] at h₇
+        obtain ⟨j, hj, hji, hjc⟩ := hS.precedes hiS₁' _ h₇
+        exact ⟨j, hj, hji.trans_le (le_of_not_lt hii'), hji, hjc⟩
+    obtain ⟨j, hj, hji, hji', hjc⟩ := this
+    have h₇ := support_f_congr h₅.symm j ?_
+    swap
+    · rw [Enumeration.smul_max, Support.comp_max_eq_of_canComp]
+      exact hji
+      exact ⟨j, hji, c, hjc⟩
+    have h₈ := support_f_congr h₆.symm j ?_
+    swap
+    · rw [Enumeration.smul_max, Support.comp_max_eq_of_canComp]
+      exact hji'
+      exact ⟨j, hji', c, hjc⟩
+    simp only [Enumeration.smul_f, Support.comp_f_eq] at h₇ h₈
+    obtain ⟨d, hd⟩ := comp_eq_same hσS hσT hj (P.B.cons P.hδ) c hjc
+    rw [Support.comp_decomp_eq _ _ (by exact hjc),
+      Support.comp_decomp_eq _ _ (by exact hd)] at h₇ h₈
+    exact h₇.trans h₈.symm
+  clear h₅ h₆
+  have hNTT' : NT.fst = NT'.fst
+  · rw [hNT, hNT', this]
+  refine NearLitter.ext ?_
+  rw [← symmDiff_eq_bot, bot_eq_empty, eq_empty_iff_forall_not_mem]
+  intro a ha
+  obtain ⟨j, hj, -, -, hja⟩ :=
+    hT.interferes hiT₁ hiT₁' hiT₂ hiT₂' (Support.Interferes.symmDiff hNTT' ha)
+  simp only [Function.funext_iff, Set.ext_iff] at h₅'
+  obtain ⟨_, _, a', NS', _, ha', hS', -⟩ :=
+    (h₅' i' j).mpr ⟨hiT₁', hj, a, NT', hNTT'.symm, ha, hiT₂', hja⟩
+  cases hiS₂'.symm.trans hS'
+  simp only [symmDiff_self, bot_eq_empty, mem_empty_iff_false] at ha'
+
+theorem convertNearLitter_subsingleton_inflexibleBot (A : ExtendedIndex β) (NS NT NT' : NearLitter)
+    (h : ConvertNearLitter S T A NS NT) (h' : ConvertNearLitter S T A NS NT')
+    (hNS : InflexibleBot A NS.1) : NT = NT' := by
+  obtain ⟨P, a, hNS⟩ := hNS
+  obtain ⟨i, hiS₁, hiT₁, hiS₂, hiT₂⟩ := h
+  obtain ⟨i', hiS₁', hiT₁', hiS₂', hiT₂'⟩ := h'
+  have h₁ := hσS.inflexibleBot_spec i hiS₁ A NS ⟨P, a, hNS⟩ hiS₂
+  have h₂ := hσS.inflexibleBot_spec i' hiS₁' A NS ⟨P, a, hNS⟩ hiS₂'
+  obtain ⟨u, hNT⟩ := convert_inflexibleBot hσS hσT P a hNS hiS₁ hiT₁ hiS₂ hiT₂
+  obtain ⟨u', hNT'⟩ := convert_inflexibleBot hσS hσT P a hNS hiS₁' hiT₁' hiS₂' hiT₂'
+  have h₃ := hσT.inflexibleBot_spec i hiT₁ A NT ⟨P, u, hNT⟩ hiT₂
+  have h₄ := hσT.inflexibleBot_spec i' hiT₁' A NT' ⟨P, u', hNT'⟩ hiT₂'
+  have h₅ := h₁.symm.trans h₃
+  have h₆ := h₂.symm.trans h₄
+  simp only [SpecCondition.inflexibleBot.injEq, heq_eq_eq, true_and] at h₅ h₆
+  obtain ⟨h₅, h₅'⟩ := h₅
+  obtain ⟨h₆, -⟩ := h₆
+  clear h₁ h₂ h₃ h₄
+  have : u = u'
+  · clear h₅'
+    have : ∃ (j : κ) (hj : j < S.max), j < i ∧ j < i' ∧ S.f j hj = ⟨P.B.cons (bot_lt_coe _), inl a⟩
+    · by_cases hii' : i < i'
+      · have h₇ := Support.Precedes.fuzzBot A NS ⟨P, a, hNS⟩
+        rw [← P.hA, ← hiS₂] at h₇
+        obtain ⟨j, hj, hji, hjc⟩ := hS.precedes hiS₁ _ h₇
+        exact ⟨j, hj, hji, hji.trans hii', hjc⟩
+      · have h₇ := Support.Precedes.fuzzBot A NS ⟨P, a, hNS⟩
+        rw [← P.hA, ← hiS₂'] at h₇
+        obtain ⟨j, hj, hji, hjc⟩ := hS.precedes hiS₁' _ h₇
+        exact ⟨j, hj, hji.trans_le (le_of_not_lt hii'), hji, hjc⟩
+    obtain ⟨j, hj, hji, hji', ha⟩ := this
+    rw [Set.ext_iff] at h₅ h₆
+    obtain ⟨_, hj₁⟩ := (h₅ j).mp ⟨hj, ha⟩
+    obtain ⟨_, hj₂⟩ := (h₆ j).mp ⟨hj, ha⟩
+    cases hj₁.symm.trans hj₂
+    rfl
+  have hNTT' : NT.fst = NT'.fst
+  · rw [hNT, hNT', this]
+  refine NearLitter.ext ?_
+  rw [← symmDiff_eq_bot, bot_eq_empty, eq_empty_iff_forall_not_mem]
+  intro a ha
+  obtain ⟨j, hj, -, -, hja⟩ :=
+    hT.interferes hiT₁ hiT₁' hiT₂ hiT₂' (Support.Interferes.symmDiff hNTT' ha)
+  simp only [Function.funext_iff, Set.ext_iff] at h₅'
+  obtain ⟨_, _, a', NS', _, ha', hS', -⟩ :=
+    (h₅' i' j).mpr ⟨hiT₁', hj, a, NT', hNTT'.symm, ha, hiT₂', hja⟩
+  cases hiS₂'.symm.trans hS'
+  simp only [symmDiff_self, bot_eq_empty, mem_empty_iff_false] at ha'
+
 theorem convertNearLitter_subsingleton (A : ExtendedIndex β) (NS NT NT' : NearLitter)
     (h : ConvertNearLitter S T A NS NT) (h' : ConvertNearLitter S T A NS NT') : NT = NT' := by
-  obtain (hNS | ⟨⟨hNS⟩⟩ | ⟨⟨P, t, hNS⟩⟩) := flexible_cases' A NS.1
+  obtain (hNS | ⟨⟨hNS⟩⟩ | ⟨⟨hNS⟩⟩) := flexible_cases' A NS.1
   · exact convertNearLitter_subsingleton_flexible hσS hσT A NS NT NT' h h' hNS
-  · obtain ⟨i, hiS₁, hiT₁, hiS₂, hiT₂⟩ := h
-    obtain ⟨i', hiS₁', hiT₁', hiS₂', hiT₂'⟩ := h'
-    sorry
-  · obtain ⟨i, hiS₁, hiT₁, hiS₂, hiT₂⟩ := h
-    obtain ⟨i', hiS₁', hiT₁', hiS₂', hiT₂'⟩ := h'
-    have h₁ := hσS.inflexibleCoe_spec i hiS₁ A NS ⟨P, t, hNS⟩ hiS₂
-    have h₂ := hσS.inflexibleCoe_spec i' hiS₁' A NS ⟨P, t, hNS⟩ hiS₂'
-    obtain ⟨u, hNT⟩ := convert_inflexibleCoe hσS hσT P t hNS hiS₁ hiT₁ hiS₂ hiT₂
-    obtain ⟨u', hNT'⟩ := convert_inflexibleCoe hσS hσT P t hNS hiS₁' hiT₁' hiS₂' hiT₂'
-    have h₃ := hσT.inflexibleCoe_spec i hiT₁ A NT ⟨P, u, hNT⟩ hiT₂
-    have h₄ := hσT.inflexibleCoe_spec i' hiT₁' A NT' ⟨P, u', hNT'⟩ hiT₂'
-    have h₅ := h₁.symm.trans h₃
-    have h₆ := h₂.symm.trans h₄
-    clear h₁ h₂ h₃ h₄
-    simp only [SpecCondition.inflexibleCoe.injEq, heq_eq_eq, CodingFunction.code_eq_code_iff,
-      true_and] at h₅ h₆
-    obtain ⟨ρ, h₅, rfl⟩ := h₅
-    obtain ⟨ρ', h₆, rfl⟩ := h₆
-    sorry
+  · exact convertNearLitter_subsingleton_inflexibleBot hσS hσT A NS NT NT' h h' hNS
+  · exact convertNearLitter_subsingleton_inflexibleCoe hσS hσT A NS NT NT' h h' hNS
 
 def convert (S T : Support β) : StructBehaviour β :=
   fun A => {

ConNF/Counting/StrongSupport.lean

@@ -346,6 +346,11 @@ theorem Strong.smul [LeLevel β] {S : Support β} (hS : S.Strong) (ρ : Allowabl
 def before (S : Support β) (i : κ) (hi : i < S.max) : Support β :=
   ⟨i, fun j hj => S.f j (hj.trans hi)⟩
 
+@[simp]
+theorem before_f (S : Support β) (i : κ) (hi : i < S.max) (j : κ) (hj : j < i) :
+    (S.before i hi).f j hj = S.f j (hj.trans hi) :=
+  rfl
+
 @[simp]
 theorem before_carrier (S : Support β) (i : κ) (hi : i < S.max) :
     (S.before i hi).carrier = {c | ∃ j hj, j < i ∧ S.f j hj = c} := by

ConNF/Structural/Support.lean

@@ -123,4 +123,9 @@ abbrev Support (α : TypeIndex) := Enumeration (Address α)
 theorem mk_support : #(Support α) = #μ :=
   mk_enumeration (mk_address α)
 
+theorem support_f_congr {S T : Support α} (h : S = T) (i : κ) (hS : i < S.max) :
+    S.f i hS = T.f i (h ▸ hS) := by
+  cases h
+  rfl
+
 end ConNF