DecSyn.soundness

The fundamental theorem

The actual proof of individual cases can be found in logrel.v

Require Import Autosubst2.unscoped Autosubst2.syntax.
Require Import fp_red logrel typing.
From Hammer Require Import Tactics.

Theorem fundamental_theorem :
  ( Γ, ⊢ Γ ⊨ Γ )
  ( Γ a A, Γ ⊢ a ∈ A Γ ⊨ a ∈ A )
  ( Γ a b A, Γ ⊢ a ≡ b ∈ A Γ ⊨ a ≡ b ∈ A )
  ( Γ a b, Γ ⊢ a ≲ b Γ ⊨ a ≲ b ).
  apply wt_mutual; eauto with sem.
  Unshelve. all : exact 0.
Qed.

Lemma synsub_to_usub : Γ (a b : PTm), Γ ⊢ a ≲ b SN a SN b Sub.R a b.
Proof. hauto lq:on rew:off use:fundamental_theorem, SemLEq_SN_Sub. Qed.