Require Import Peano_dec.
Require Import Compare_dec.
Require Import Lt.
Require Import List.

Require Import base final_result.

Module Msorts <: term_sig.
Inductive iSorts : Set :=
 | U : iSorts
 | V : iSorts
 | V' : iSorts
 | W : iSorts
 | W': iSorts
 .

Definition Sorts := iSorts.
End Msorts.

Module Mpts <: pts_sig Msorts.
Import Msorts.
Inductive iAx : Sorts -> Sorts -> Prop :=
 | Ax0 : iAx U V
 | Ax1 : iAx U V'
 | Ax2 : iAx V W
 | Ax3 : iAx V' W'
.

Inductive iRel : Sorts -> Sorts -> Sorts -> Prop :=
 | Rel0 : iRel W W W
 | Rel1 : iRel W' W' W'
 | Rel2 : iRel V V U
 | Rel3 : iRel V' V' U.

Definition Ax := iAx.
Definition Rel := iRel.
End Mpts.

Module CE <: Theory Msorts Mpts.
Import Msorts Mpts.
Include Theory Msorts Mpts.

Hint Constructors iAx iRel.
Hint Unfold Ax Rel.

Definition PTSe_PiInj := forall Γ A B C D u, Γ ⊢e Π(A),B = Π(C),D : !u -> exists s, exists t, Rel s t u /\
 Γ ⊢e A = C : !s /\ A::Γ ⊢e B = D : !t.

Definition D1 := (λ[!V],#0)·!U. Lemma D1_ok : nil ⊢e D1 : !V.

Lemma D1_typ : forall T, nil ⊢e D1 : T -> T ≡ !V.

Definition D2 := (λ[!V'],#0)·!U. Lemma D2_ok : nil ⊢e D2 : !V'.

Lemma D2_typ : forall T, nil ⊢e D2 : T -> T ≡ !V'.

Lemma ze_pi_eq : nil ⊢e Π(D1),!U = Π(D2),!U : !U.

Lemma Dom_ce : forall s, nil ⊢e D1 = D2 : !s -> False.

Lemma PTSe_dont_have_PiInj : ~ PTSe_PiInj .

End CE.