Prove satisfiability of τε.

There is a small error in the paper. It claims that L⊨τε if and only if L≈{ε}.
However, from `⊨-anticongˡ` and `≤-min`, we have ∅⊨{ε}.

1 files changed, 23 insertions, 0 deletions

diff --git a/src/Cfe/Type/Properties.agda b/src/Cfe/Type/Properties.agda
index 14e871b..987e41f 100644
--- a/src/Cfe/Type/Properties.agda
+++ b/src/Cfe/Type/Properties.agda
@@ -45,3 +45,26 @@ L⊨τ⊥⇒L≈∅ {L = L} L⊨τ⊥ = record
   ; f⇒f = λ ()
   ; l⇒l = λ ()
   }
+
+L⊨τε⇒L≤｛ε｝ : ∀ {a aℓ} {L : Language a aℓ} → L ⊨ τε → L ≤ ｛ε｝
+L⊨τε⇒L≤｛ε｝{L = L} L⊨τε = record
+  { f = λ {l} l∈L → elim l l∈L
+  ; cong = λ {l₁} {l₂} {l₁∈L} {l₂∈L} l₁≈l₂ → tt
+  }
+  where
+  open import Data.Unit
+  open import Relation.Binary.PropositionalEquality
+  module L⊨τε = _⊨_ L⊨τε
+
+  elim : ∀ l (l∈L : l ∈ L) → l ∈ ｛ε｝
+  elim [] []∈L = refl
+  elim (x ∷ l) xl∈L = ⊥-elim (L⊨τε.f⇒f (-, xl∈L))
+
+｛ε｝⊨τε : ｛ε｝ ⊨ τε
+｛ε｝⊨τε = record
+  { n⇒n = const tt
+  ; f⇒f = λ ()
+  ; l⇒l = λ { ([] , ()) ; (_ ∷ _ , ())}
+  }
+  where
+  open import Data.Unit