Library CoC_BetaStar
Require Import Metatheory CoC_Definitions CoC_Infrastructure.
Generalities on relations
Lemma red_all_to_out : forall (R : relation),
red_all R -> red_refl R -> red_out R.
Lemma red_out_to_rename : forall (R : relation),
red_out R -> red_rename R.
Lemma red_all_to_through : forall (R : relation),
red_regular R -> red_all R -> red_through R.
Properties of beta relation
Lemma beta_red_out : red_out beta.
Lemma beta_red_rename : red_rename beta.
Properties of beta star relation
Lemma beta_star_app1 : forall t1 t1' t2,
(beta star) t1 t1' -> term t2 ->
(beta star) (trm_app t1 t2) (trm_app t1' t2).
Lemma beta_star_app2 : forall t1 t2 t2',
(beta star) t2 t2' -> term t1 ->
(beta star) (trm_app t1 t2) (trm_app t1 t2').
Lemma beta_star_abs1 : forall t1 t1' t2,
(beta star) t1 t1' -> body t2 ->
(beta star) (trm_abs t1 t2) (trm_abs t1' t2).
Lemma beta_star_prod1 : forall t1 t1' t2,
(beta star) t1 t1' -> body t2 ->
(beta star) (trm_prod t1 t2) (trm_prod t1' t2).
Lemma beta_star_abs2 : forall L t1 t2 t2',
term t1 ->
(forall x, x \notin L -> (beta star) (t2 ^ x) (t2' ^ x)) ->
(beta star) (trm_abs t1 t2) (trm_abs t1 t2').
Lemma beta_star_prod2 : forall L t1 t2 t2',
term t1 ->
(forall x, x \notin L -> (beta star) (t2 ^ x) (t2' ^ x)) ->
(beta star) (trm_prod t1 t2) (trm_prod t1 t2').
Lemma beta_star_red_in : red_in (beta star).
Lemma beta_star_red_all : red_all (beta star).
Lemma beta_star_red_through : red_through (beta star).