(* This file was automatically generated: do not edit *********************)
-include "Basic-1/pr1/props.ma".
+include "basic_1/pr1/props.ma".
-include "Basic-1/pr0/pr0.ma".
+include "basic_1/pr0/pr0.ma".
-theorem pr1_strip:
+lemma pr1_strip:
\forall (t0: T).(\forall (t1: T).((pr1 t0 t1) \to (\forall (t2: T).((pr0 t0
t2) \to (ex2 T (\lambda (t: T).(pr1 t1 t)) (\lambda (t: T).(pr1 t2 t)))))))
\def
x0)).(ex_intro2 T (\lambda (t: T).(pr1 t4 t)) (\lambda (t: T).(pr1 t5 t)) x0
H7 (pr1_t x t5 (pr1_pr0 t5 x H4) x0 H8))))) H6))))) (pr0_confluence t3 t5 H3
t2 H0)))))))))) t0 t1 H))).
-(* COMMENTS
-Initial nodes: 317
-END *)
theorem pr1_confluence:
\forall (t0: T).(\forall (t1: T).((pr1 t0 t1) \to (\forall (t2: T).((pr1 t0
t))) (\lambda (x0: T).(\lambda (H8: (pr1 t4 x0)).(\lambda (H9: (pr1 x
x0)).(ex_intro2 T (\lambda (t: T).(pr1 t4 t)) (\lambda (t: T).(pr1 t5 t)) x0
H8 (pr1_t x t5 H5 x0 H9))))) H7)))))) H4))))))))))) t0 t1 H))).
-(* COMMENTS
-Initial nodes: 311
-END *)