some reorganization and some corrections

[helm.git] / helm / coq-contribs / LAMBDA-TYPES / pc3_defs.v

diff --git a/helm/coq-contribs/LAMBDA-TYPES/pc3_defs.v b/helm/coq-contribs/LAMBDA-TYPES/pc3_defs.v
index b2b530d599a66d093067b2aa877656aec98cd3f8..ada99cf2c0a0c20c5fe1a308b86b5938865cffec 100644 (file)
--- a/helm/coq-contribs/LAMBDA-TYPES/pc3_defs.v
+++ b/helm/coq-contribs/LAMBDA-TYPES/pc3_defs.v
@@ -1,20 +1,29 @@
-(*#* #stop file *)
-
 Require Export pr2_defs.
 Require Export pr3_defs.
 Require Export pc1_defs.
 
+(*#* #stop file *)
+
       Inductive pc2 [c:C; t1,t2:T] : Prop :=
          | pc2_r : (pr2 c t1 t2) -> (pc2 c t1 t2)
          | pc2_x : (pr2 c t2 t1) -> (pc2 c t1 t2).
 
       Hint pc2 : ltlc := Constructors pc2.
 
+(*#* #start file *)
+
+(*#* #caption "axioms for the relation $\\PcT{}{}{}$",
+   "reflexivity", "single step transitivity" 
+*)
+(*#* #cap #cap c, t, t1, t2, t3 *)
+
       Inductive pc3 [c:C] : T -> T -> Prop :=
          | pc3_r : (t:?) (pc3 c t t)
          | pc3_u : (t2,t1:?) (pc2 c t1 t2) ->
                    (t3:?) (pc3 c t2 t3) -> (pc3 c t1 t3).
 
+(*#* #stop file *)
+
       Hint pc3 : ltlc := Constructors pc3.
 
    Section pc2_props. (******************************************************)
@@ -156,5 +165,8 @@ Require Export pc1_defs.
                LApply (pc3_t (TTail ?3 ?4 ?5) ?1 ?2); [ Intros H_x | XAuto ];
                LApply (H_x (TTail ?3 ?6 ?5)); [ Clear H_x; Intros | Apply pc3_s; XAuto ]
             | [ _: (pc3 ?1 ?2 ?3); _: (pr3 ?1 ?3 ?4) |- ? ] ->
+               LApply (pc3_t ?3 ?1 ?2); [ Intros H_x | XAuto ];
+               LApply (H_x ?4); [ Clear H_x; Intros | XAuto ]
+            | [ _: (pc3 ?1 ?2 ?3); _: (pc3 ?1 ?4 ?3) |- ? ] ->
                LApply (pc3_t ?3 ?1 ?2); [ Intros H_x | XAuto ];
                LApply (H_x ?4); [ Clear H_x; Intros | XAuto ].