+
+ Section pc3_ind_left. (***************************************************)
+
+ Inductive pc3_left [c:C] : T -> T -> Prop :=
+ | pc3_left_r : (t:?) (pc3_left c t t)
+ | pc3_left_ur: (t1,t2:?) (pr2 c t1 t2) -> (t3:?) (pc3_left c t2 t3) ->
+ (pc3_left c t1 t3)
+ | pc3_left_ux: (t1,t2:?) (pr2 c t1 t2) -> (t3:?) (pc3_left c t1 t3) ->
+ (pc3_left c t2 t3).
+
+ Hint pc3_left: ltlc := Constructors pc3_left.
+
+ Remark pc3_left_pr3: (c:?; t1,t2:?) (pr3 c t1 t2) -> (pc3_left c t1 t2).
+ Intros; XElim H; XEAuto.
+ Qed.
+
+ Remark pc3_left_trans: (c:?; t1,t2:?) (pc3_left c t1 t2) ->
+ (t3:?) (pc3_left c t2 t3) -> (pc3_left c t1 t3).
+ Intros until 1; XElim H; XEAuto.
+ Qed.
+
+ Hints Resolve pc3_left_trans : ltlc.
+
+ Remark pc3_left_sym: (c:?; t1,t2:?) (pc3_left c t1 t2) ->
+ (pc3_left c t2 t1).
+ Intros; XElim H; XEAuto.
+ Qed.
+
+ Hints Resolve pc3_left_sym pc3_left_pr3 : ltlc.
+
+ Remark pc3_left_pc3: (c:?; t1,t2:?) (pc3 c t1 t2) -> (pc3_left c t1 t2).
+ Intros; Pc3Unfold; XEAuto.
+ Qed.
+
+ Remark pc3_pc3_left: (c:?; t1,t2:?) (pc3_left c t1 t2) -> (pc3 c t1 t2).
+ Intros; XElim H; XEAuto.
+ Qed.
+
+ Hints Resolve pc3_left_pc3 pc3_pc3_left : ltlc.
+
+ Theorem pc3_ind_left: (c:C; P:(T->T->Prop))
+ ((t:T) (P t t)) ->
+ ((t1,t2:T) (pr2 c t1 t2) -> (t3:T) (pc3 c t2 t3) -> (P t2 t3) -> (P t1 t3)) ->
+ ((t1,t2:T) (pr2 c t1 t2) -> (t3:T) (pc3 c t1 t3) -> (P t1 t3) -> (P t2 t3)) ->
+ (t,t0:T) (pc3 c t t0) -> (P t t0).
+ Intros; ElimType (pc3_left c t t0); XEAuto.
+ Qed.
+
+ End pc3_ind_left.