- Inductive pc1 : T -> T -> Prop :=
- | pc1_r : (t:?) (pc1 t t)
- | pc1_u : (t2,t1:?) (pc0 t1 t2) -> (t3:?) (pc1 t2 t3) -> (pc1 t1 t3).
-
- Hint pc1 : ltlc := Constructors pc1.
-
- Section pc0_props. (******************************************************)
-
- Theorem pc0_s : (t2,t1:?) (pc0 t1 t2) -> (pc0 t2 t1).
- Intros.
- Inversion H; XAuto.
- Qed.
-
- End pc0_props.
-
- Hints Resolve pc0_s : ltlc.