some reorganization and some corrections

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

diff --git a/helm/coq-contribs/LAMBDA-TYPES/fsubst0_defs.v b/helm/coq-contribs/LAMBDA-TYPES/fsubst0_defs.v
new file mode 100644 (file)
index 0000000..c7382bf
--- /dev/null
+++ b/helm/coq-contribs/LAMBDA-TYPES/fsubst0_defs.v
@@ -0,0 +1,20 @@
+Require Export subst0_defs.
+Require Export csubst0_defs.
+
+(*#* #caption "axioms for strict substitution in focalized terms",
+   "substituted term part", 
+   "substituted context part", 
+   "substituted both parts"
+*)
+(*#* #cap #cap c1, c2, t1, t2 #alpha v in W *)  
+
+      Inductive fsubst0 [i:nat; v:T; c1:C; t1:T] : C -> T -> Prop :=
+         | fsubst0_snd : (t2:?) (subst0 i v t1 t2) -> (fsubst0 i v c1 t1 c1 t2)
+         | fsubst0_fst : (c2:?) (csubst0 i v c1 c2) -> (fsubst0 i v c1 t1 c2 t1)
+         | fsubst0_both : (t2:?) (subst0 i v t1 t2) ->
+                       (c2:?) (csubst0 i v c1 c2) -> (fsubst0 i v c1 t1 c2 t2).
+
+(*#* #stop file *)
+
+      Hint fsubst0 : ltlc := Constructors fsubst0.
+