Library Lambda.TPOSR.RightReflexivity


Require
 Import
 Lambda.TPOSR.Terms.

Require
 Import
 Lambda.TPOSR.Reduction.

Require
 Import
 Lambda.TPOSR.Conv.

Require
 Import
 Lambda.TPOSR.LiftSubst.

Require
 Import
 Lambda.TPOSR.Env.

Require
 Import
 Lambda.TPOSR.Types.

Require
 Import
 Lambda.TPOSR.LeftReflexivity.

Require
 Import
 Lambda.TPOSR.CtxReduction.

Require
 Import
 Lambda.TPOSR.PreCtxCoercion.

Require
 Import
 Lambda.TPOSR.Substitution.

Require
 Import
 Lambda.TPOSR.PreSubstitutionTPOSR.







Implicit
 Types
 i
 k
 m
 n
 p
 : nat.

Implicit
 Type
 s
 : sort.

Implicit
 Types
 A
 B
 M
 N
 T
 t
 u
 v
 : lterm.

Implicit
 Types
 e
 f
 g
 : lenv.




Lemma
 tposr_pair_red_left_aux : ∀ e
 t
 u
 T
, e
 |-- t
 -> u
 : T
 ->

  ∀ A
 B
 a
 b
, t
 = Pair_l (Sum_l A
 B
) a
 b
 -> 

  u
 = t
 ->

  e
 |-- a
 -> a
 : A
.




Lemma
 tposr_pair_red_left : ∀ e
 A
 B
 a
 b
 T
, e
 |-- Pair_l (Sum_l A
 B
) a
 b
 -> Pair_l (Sum_l A
 B
) a
 b
 : T
 ->

  e
 |-- a
 -> a
 : A
.




Lemma
 tposr_pair_red_comp_aux : ∀ e
 t
 u
 T
, e
 |-- t
 -> u
 : T
 ->

  ∀ A
 B
 a
 b
, t
 = Pair_l (Sum_l A
 B
) a
 b
 -> 

  ∀ A'
 B'
 a'
 b'
, u
 = Pair_l (Sum_l A'
 B'
) a'
 b'
 ->

  e
 |-- a
 -> a'
 : A
 ∧ e
 |-- b
 -> b'
 : lsubst a
 B
.




Lemma
 tposr_pair_red_comp : ∀ e
 A
 B
 a
 b
 A'
 B'
 a'
 b'
 T
, e
 |-- Pair_l (Sum_l A
 B
) a
 b
 -> Pair_l (Sum_l A'
 B'
) a'
 b'
 : T
 ->

  e
 |-- a
 -> a'
 : A
 ∧ e
 |-- b
 -> b'
 : lsubst a
 B
.




Lemma
 tposr_pair_coerce_left_aux : ∀ e
 t
 u
 T
, e
 |-- t
 -> u
 : T
 ->

  ∀ A
 B
 a
 b
, t
 = Pair_l (Sum_l A
 B
) a
 b
 -> 

  ∀ A'
 B'
 a'
 b'
, u
 = Pair_l (Sum_l A'
 B'
) a'
 b'
 ->

  ∃ s
 : sort, e
 |-- A
 -> A'
 : s
.




Lemma
 tposr_pair_coerce_left : ∀ e
 A
 B
 a
 b
 A'
 B'
 a'
 b'
 T
, e
 |-- Pair_l (Sum_l A
 B
) a
 b
 -> Pair_l (Sum_l A'
 B'
) a'
 b'
 : T
 ->

  ∃ s
 : sort, e
 |-- A
 -> A'
 : s
.




Lemma
 tposr_pair_red_right_aux : ∀ e
 t
 u
 T
, e
 |-- t
 -> u
 : T
 ->

  ∀ A
 B
 a
 b
, t
 = Pair_l (Sum_l A
 B
) a
 b
 -> u
 = t
 ->

  e
 |-- b
 -> b
 : lsubst a
 B
.




Lemma
 tposr_pair_red_right : ∀ e
 A
 B
 a
 b
 T
, e
 |-- Pair_l (Sum_l A
 B
) a
 b
 -> Pair_l (Sum_l A
 B
) a
 b
 : T
 ->

  e
 |-- b
 -> b
 : lsubst a
 B
.




Lemma
 tposr_pair_coerce_right_aux : ∀ e
 t
 u
 T
, e
 |-- t
 -> u
 : T
 ->

  ∀ A
 B
 a
 b
, t
 = Pair_l (Sum_l A
 B
) a
 b
 -> 

  ∀ A'
 B'
 a'
 b'
, u
 = Pair_l (Sum_l A'
 B'
) a'
 b'
 ->

  ∃ s
 : sort, (A
 :: e
) |-- B
 -> B'
 : s
.




Lemma
 tposr_pair_coerce_right : ∀ e
 A
 B
 a
 b
 A'
 B'
 a'
 b'
 T
, e
 |-- Pair_l (Sum_l A
 B
) a
 b
 -> Pair_l (Sum_l A'
 B'
) a'
 b'
 : T
 ->

  ∃ s
 : sort, (A
 :: e
) |-- B
 -> B'
 : s
.




Lemma
 ind_right_refl : 

  (∀ e
 u
 v
 T
, e
 |-- u
 -> v
 : T
 -> e
 |-- v
 -> v
 : T
) ∧

  (∀ e
, tposr_wf e
 -> True) ∧

  (∀ e
 u
 v
 s
, e
 |-- u
 ~= v
 : s
 -> 

  e
 |-- u
 -> u
 : s
 ∧ e
 |-- v
 -> v
 : s
) ∧

  (∀ e
 u
 v
 s
, e
 |-- u
 >-> v
 : s
 ->

  e
 |-- u
 -> u
 : s
 ∧ e
 |-- v
 -> v
 : s
).




Corollary
 refl_r : ∀ e
 u
 v
 T
, e
 |-- u
 -> v
 : T
 -> e
 |-- v
 -> v
 : T
.




Corollary
 tposrp_refl_r : ∀ e
 A
 B
 T
, tposrp e
 A
 B
 T
 -> e
 |-- B
 -> B
 : T
.




Corollary
 eq_refls : ∀ e
 u
 v
 s
, e
 |-- u
 ~= v
 : s
 -> e
 |-- u
 -> u
 : s
 ∧ e
 |-- v
 -> v
 : s
.




Corollary
 eq_refl_l : ∀ e
 u
 v
 s
, e
 |-- u
 ~= v
 : s
 -> e
 |-- u
 -> u
 : s
.




Corollary
 eq_refl_r : ∀ e
 u
 v
 s
, e
 |-- u
 ~= v
 : s
 -> e
 |-- v
 -> v
 : s
.




Corollary
 coerce_refls : ∀ e
 u
 v
 s
, e
 |-- u
 >-> v
 : s
 -> e
 |-- u
 -> u
 : s
 ∧ e
 |-- v
 -> v
 : s
.




Corollary
 coerce_refl_l : ∀ e
 u
 v
 s
, e
 |-- u
 >-> v
 : s
 -> e
 |-- u
 -> u
 : s
.




Corollary
 coerce_refl_r : ∀ e
 u
 v
 s
, e
 |-- u
 >-> v
 : s
 -> e
 |-- v
 -> v
 : s
.




Hint
 Resolve
 refl_r tposrp_refl_r eq_refl_l eq_refl_r coerce_refl_l coerce_refl_r : coc
.