Skip to content

Instantly share code, notes, and snippets.

@calebmer

calebmer/proof.txt

Last active February 15, 2019 00:30
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save calebmer/859489101db22a5e5c36bc29310c1f7c to your computer and use it in GitHub Desktop.
Save calebmer/859489101db22a5e5c36bc29310c1f7c to your computer and use it in GitHub Desktop.
Download ZIP
Raw
proof.txt
∀(∅) ∀b.T b ⊑ ∀b.T b
───────────────────────── (Eq-Free)
∀(∅) ∀(b, b).T b ⊑ ∀b.T b
───────────────────────── (R-Context)
∀(b) ∀b.T b ⊑ T b
─────────────────────────────────────── (I-Context)
∀(b) ∀(a ≥ ∀b.T b).T a ⊑ ∀(a ≥ T b).T a
───────────────────────────────────────────── (R-Context)
∀(∅) ∀(b, a ≥ ∀b.T b).T a ⊑ ∀(b, a ≥ T b).T a
───────────────────────────────────────────── (Eq-Free)
∀(∅) ∀(a ≥ ∀b.T b).T a ⊑ ∀(b, a ≥ T b).T a
────────────────────────────────────────── (Eq-Mono)
∀(∅) ∀(a ≥ ∀b.T b).T a ⊑ ∀b.T (T b)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment