include "basic_1/pr1/pr1.ma".
-theorem pc1_pr0_r:
+lemma pc1_pr0_r:
\forall (t1: T).(\forall (t2: T).((pr0 t1 t2) \to (pc1 t1 t2)))
\def
\lambda (t1: T).(\lambda (t2: T).(\lambda (H: (pr0 t1 t2)).(ex_intro2 T
(\lambda (t: T).(pr1 t1 t)) (\lambda (t: T).(pr1 t2 t)) t2 (pr1_pr0 t1 t2 H)
(pr1_refl t2)))).
-theorem pc1_pr0_x:
+lemma pc1_pr0_x:
\forall (t1: T).(\forall (t2: T).((pr0 t2 t1) \to (pc1 t1 t2)))
\def
\lambda (t1: T).(\lambda (t2: T).(\lambda (H: (pr0 t2 t1)).(ex_intro2 T
(\lambda (t: T).(pr1 t1 t)) (\lambda (t: T).(pr1 t2 t)) t1 (pr1_refl t1)
(pr1_pr0 t2 t1 H)))).
-theorem pc1_refl:
+lemma pc1_refl:
\forall (t: T).(pc1 t t)
\def
\lambda (t: T).(ex_intro2 T (\lambda (t0: T).(pr1 t t0)) (\lambda (t0:
T).(pr1 t t0)) t (pr1_refl t) (pr1_refl t)).
-theorem pc1_pr0_u:
+lemma pc1_pr0_u:
\forall (t2: T).(\forall (t1: T).((pr0 t1 t2) \to (\forall (t3: T).((pc1 t2
t3) \to (pc1 t1 t3)))))
\def
(t: T).(pr1 t1 t)) (\lambda (t: T).(pr1 t3 t)) x (pr1_sing t2 t1 H x H2)
H3)))) H1)))))).
-theorem pc1_s:
+lemma pc1_s:
\forall (t2: T).(\forall (t1: T).((pc1 t1 t2) \to (pc1 t2 t1)))
\def
\lambda (t2: T).(\lambda (t1: T).(\lambda (H: (pc1 t1 t2)).(let H0 \def H in
x)).(ex_intro2 T (\lambda (t: T).(pr1 t2 t)) (\lambda (t: T).(pr1 t1 t)) x H2
H1)))) H0)))).
-theorem pc1_head_1:
+lemma pc1_head_1:
\forall (u1: T).(\forall (u2: T).((pc1 u1 u2) \to (\forall (t: T).(\forall
(k: K).(pc1 (THead k u1 t) (THead k u2 t))))))
\def
t) t0)) (THead k x t) (pr1_head_1 u1 x H1 t k) (pr1_head_1 u2 x H2 t k)))))
H0)))))).
-theorem pc1_head_2:
+lemma pc1_head_2:
\forall (t1: T).(\forall (t2: T).((pc1 t1 t2) \to (\forall (u: T).(\forall
(k: K).(pc1 (THead k u t1) (THead k u t2))))))
\def
(pr1_t x0 t1 H5 x1 H7) (pr1_t x t3 H3 x1 H8))))) (pr1_confluence t2 x0 H6 x
H2))))) H4))))) H1)))))).
-theorem pc1_pr0_u2:
+lemma pc1_pr0_u2:
\forall (t0: T).(\forall (t1: T).((pr0 t0 t1) \to (\forall (t2: T).((pc1 t0
t2) \to (pc1 t1 t2)))))
\def