Library Lambda.TPOSR.Transitivity


Require
 Import
 Lambda.Utils.

Require
 Import
 Lambda.Tactics.




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.Basic.

Require
 Import
 Lambda.TPOSR.Thinning.

Require
 Import
 Lambda.TPOSR.Substitution.

Require
 Import
 Lambda.TPOSR.RightReflexivity.

Require
 Import
 Lambda.TPOSR.CtxCoercion.

Require
 Import
 Lambda.TPOSR.Generation.

Require
 Import
 Lambda.TPOSR.UnicityOfSorting.

Require
 Import
 Lambda.TPOSR.ChurchRosser.

Require
 Import
 Lambda.TPOSR.CoerceDepth.

Require
 Import
 Lambda.TPOSR.CoerceNoTrans.

Require
 Import
 Lambda.TPOSR.TransitivitySet.







Implicit
 Types
 i
 k
 m
 n
 p
 : nat.

Implicit
 Type
 s
 : sort.

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




Theorem
 coerces_trans : ∀ e
 A
 B
 C
 s
, e
 |-- A
 >>> B
 : s
 -> e
 |-- B
 >>> C
 : s
 ->

  e
 |-- A
 >>> C
 : s
.




Require
 Import
 Lambda.TPOSR.CoerceDepth.




Theorem
 coerce_rc_depth_trans : ∀ e
 A
 B
 C
 s
 n1
 n2
, e
 |-- A
 >-> B
 : s
 [n1
] -> e
 |-- B
 >-> C
 : s
 [n2
]->

  ∃ m
, e
 |-- A
 >-> C
 : s
 [m
].




Theorem
 coerce_rc_depth_sym : ∀ e
 A
 B
 s
 n
, e
 |-- A
 >-> B
 : s
 [n
] ->

  e
 |-- B
 >-> A
 : s
 [n
].




Theorem
 coerce_coerce_rc_depth : ∀ e
 A
 B
 s
, e
 |-- A
 >-> B
 : s
 -> ∃ n
, e
 |-- A
 >-> B
 : s
 [n
].