helm/coq-contribs/LAMBDA-TYPES/fsubst0_defs.v

   1 Require Export subst0_defs.
   2 Require Export csubst0_defs.
   3
   4 (*#* #caption "\\kern-1.2pt axioms for strict substitution in focalized terms",
   5    "substituted term part",
   6    "substituted context part",
   7    "substituted both parts"
   8 *)
   9 (*#* #cap #cap c1, c2, t1, t2 #alpha v in W *)
  10
  11       Inductive fsubst0 [i:nat; v:T; c1:C; t1:T] : C -> T -> Prop :=
  12          | fsubst0_snd : (t2:?) (subst0 i v t1 t2) -> (fsubst0 i v c1 t1 c1 t2)
  13          | fsubst0_fst : (c2:?) (csubst0 i v c1 c2) -> (fsubst0 i v c1 t1 c2 t1)
  14          | fsubst0_both : (t2:?) (subst0 i v t1 t2) ->
  15                        (c2:?) (csubst0 i v c1 c2) -> (fsubst0 i v c1 t1 c2 t2).
  16
  17 (*#* #stop file *)
  18
  19       Hint fsubst0 : ltlc := Constructors fsubst0.
  20