Library Lambda.TPOSR.CtxConversion
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.CtxCoercion.
Require Import Lambda.TPOSR.RightReflexivity.
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.
Inductive conv_in_env : lenv -> lenv -> Prop :=
| conv_env_hd : ∀ e t u s, e |-- t ~= u : s ->
conv_in_env (t :: e) (u :: e)
| conv_env_tl :
∀ e f t, conv_in_env e f -> conv_in_env (t :: e) (t :: f).
Hint Resolve conv_env_hd conv_env_tl: coc.
Lemma conv_in_env_coerce_in_env : ∀ e f, conv_in_env e f -> tposr_wf e -> coerce_in_env e f.
Hint Resolve conv_in_env_coerce_in_env : coc.
Lemma conv_env :
(∀ e t u T, e |-- t -> u : T ->
∀ f, conv_in_env e f -> f |-- t -> u : T).
Corollary eq_conv_env :
(∀ e t u s, e |-- t ~= u : s ->
∀ f, conv_in_env e f -> f |-- t ~= u : s).
Corollary coerce_conv_env :
(∀ e t u s, e |-- t >-> u : s ->
∀ f, conv_in_env e f -> f |-- t >-> u : s).
Lemma conv_in_env_sym : ∀ e f, conv_in_env e f -> conv_in_env f e.
Hint Resolve conv_in_env_sym : coc.