(****************************************************************************)
(*                                                                          *)
(*                The formal system \lambda\delta                           *)
(*                                                                          *)
(*                Author: Ferruccio Guidi                                   *)
(*                                                                          *)
(*                This file is distributed under the terms of the           *)
(*                GNU General Public License Version 2                      *)
(*                                                                          *)
(****************************************************************************)

Require Export subst0_defs.
Require Export csubst0_defs.

      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).

      Hint fsubst0 : ld := Constructors fsubst0.

   Section fsubst0_gen_base. (***********************************************)

      Lemma fsubst0_gen_base: (c1,c2:?; t1,t2,v:?; i:?)
                              (fsubst0 i v c1 t1 c2 t2) -> (OR
                              c1 = c2 /\ (subst0 i v t1 t2) |
                              t1 = t2 /\ (csubst0 i v c1 c2) |
                              (subst0 i v t1 t2) /\ (csubst0 i v c1 c2)).
      Proof.
      Intros; XElim H; XAuto.
      Qed.

   End fsubst0_gen_base.

      Tactic Definition FSubst0GenBase := (
         Match Context With
            | [ H: (fsubst0 ?1 ?2 ?3 ?4 ?5 ?6) |- ? ] ->
               XDecomPoseClear H '(fsubst0_gen_base ? ? ? ? ? ? H)
         ).