Library Conv
Require Export Term.
Section Church_Rosser.
Definition str_confluent R := commut _ R (transp term R).
Lemma str_confluence_par_red1 : str_confluent par_red1.
Lemma strip_lemma : commut _ par_red (transp _ par_red1).
Lemma confluence_par_red : str_confluent par_red.
Lemma confluence_red : str_confluent red.
Theorem church_rosser :
forall u v, conv u v -> exists2 t, red u t & red v t.
Lemma inv_conv_prod_l :
forall a b c d, conv (Prod a c) (Prod b d) -> conv a b.
Lemma inv_conv_prod_r :
forall a b c d, conv (Prod a c) (Prod b d) -> conv c d.
Lemma nf_uniqueness : forall u v, conv u v -> normal u -> normal v -> u = v.
Lemma conv_sort : forall s1 s2, conv (Srt s1) (Srt s2) -> s1 = s2.
Lemma conv_kind_prop : ~ conv (Srt kind) (Srt prop).
Lemma conv_sort_prod : forall s t u, ~ conv (Srt s) (Prod t u).
End Church_Rosser.