Library CoC_BetaStar

Require Import Metatheory CoC_Definitions CoC_Infrastructure.


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.


Lemma beta_red_out : red_out beta.

Lemma beta_red_rename : red_rename beta.


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



---

Index

---

This page has been generated by coqdoc