Require MinMJ_Lift.
Require MinMJ_Drop.

(* Support functions for Phi. *)

(* subst a for i in (var j). *)
Recursive Definition
    VsubstAV : A->V->V->A :=
	a i j => (Setifb A (nateqb i j) a (var (drop_V i j))).

Fixpoint
    NsubstAV1 [n:N]: A->nat->N :=
	[a:A][i:nat]<N>Case n of
	    (* lam n *)[n':N]
		(lam (NsubstAV1 n' (lift_A O a) (S i)))
	    (* an a *)[a':A]
		(an (AsubstAV1 a' a i))
end with
    AsubstAV1 [a:A] : A->nat->A :=
	[a':A][i:nat]<A>Case a of
	    (* ap a n *)[a'':A][n:N]
		(ap (AsubstAV1 a'' a' i) (NsubstAV1 n a' i))
	    (* var x *)[x:V]
		(VsubstAV a' i x)
end.

Recursive Definition
    NsubstAV : A->V->N->N :=
	a i n => (NsubstAV1 n a i).

Recursive Definition
    AsubstAV : A->V->A->A :=
	a i a' => (AsubstAV1 a' a i).

Lemma NSAV1 : (a:A)(i:nat)(n:N)
		((NsubstAV a i (lam n)) =
		 (lam (NsubstAV (lift_A O a) (S i) n))).
Auto.
Save.

Lemma NSAV2 : (a:A)(i:nat)(a':A)
		((NsubstAV a i (an a')) =
		 (an (AsubstAV a i a'))).
Auto.
Save.

Lemma NSAV3 : (a:A)(i:nat)(a':A)(n:N)
		((AsubstAV a i (ap a' n)) =
		 (ap (AsubstAV a i a') (NsubstAV a i n))).
Auto.
Save.

Lemma NSAV4 : (a:A)(i:nat)(x:V)
		((AsubstAV a i (var x)) =
		 (VsubstAV a i x)).
Auto.
Save.