(* This file was automatically generated: do not edit *********************)
-include "Basic-1/ty3/arity_props.ma".
+include "basic_1/ty3/arity_props.ma".
-include "Basic-1/nf2/fwd.ma".
+include "basic_1/nf2/fwd.ma".
theorem pc3_dec:
\forall (g: G).(\forall (c: C).(\forall (u1: T).(\forall (t1: T).((ty3 g c
(eq_ind_r T x2 (\lambda (t: T).(pr3 c x1 t)) H15 x0 H_y1) in (let H17 \def
(nf2_pr3_confluence c x H3 x0 H6 u1 H2) in (H8 (H17 (pr3_t x1 u1 c H11 x0
H16)) False))))))) H13)))))) H10))))) H7)))))) H4)))))) H1)))))))))))).
-(* COMMENTS
-Initial nodes: 551
-END *)
theorem pc3_abst_dec:
\forall (g: G).(\forall (c: C).(\forall (u1: T).(\forall (t1: T).((ty3 g c
(Bind Abst)) (H32 (pr3_t x3 u2 c H20 x5 H25)) (refl_equal T x6))) False))))
H29))))))))) H23)))))))) H18))))))) (pr3_confluence c u1 x1 H13 x H4)))))
H12)))))) H9)))))) H6)))))) H3)))))))))))).
-(* COMMENTS
-Initial nodes: 1759
-END *)