theory LFex
imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../QuotMain"  "Abs"
begin

atom_decl name
atom_decl ident

datatype kind =
    Type
  | KPi "ty" "name" "kind"
and ty =
    TConst "ident"
  | TApp "ty" "trm"
  | TPi "ty" "name" "ty"
and trm =
    Const "ident"
  | Var "name"
  | App "trm" "trm"
  | Lam "ty" "name" "trm"
print_theorems

primrec
    rfv_kind :: "kind \<Rightarrow> atom set"
and rfv_ty   :: "ty \<Rightarrow> atom set"
and rfv_trm  :: "trm \<Rightarrow> atom set"
where
  "rfv_kind (Type) = {}"
| "rfv_kind (KPi A x K) = (rfv_ty A) \<union> ((rfv_kind K) - {atom x})"
| "rfv_ty (TConst i) = {}"
| "rfv_ty (TApp A M) = (rfv_ty A) \<union> (rfv_trm M)"
| "rfv_ty (TPi A x B) = (rfv_ty A) \<union> ((rfv_ty B) - {atom x})"
| "rfv_trm (Const i) = {}"
| "rfv_trm (Var x) = {atom x}"
| "rfv_trm (App M N) = (rfv_trm M) \<union> (rfv_trm N)"
| "rfv_trm (Lam A x M) = (rfv_ty A) \<union> ((rfv_trm M) - {atom x})"

instantiation kind and ty and trm :: pt
begin

primrec
    permute_kind
and permute_ty
and permute_trm
where
  "permute_kind pi Type = Type"
| "permute_kind pi (KPi t n k) = KPi (permute_ty pi t) (pi \<bullet> n) (permute_kind pi k)"
| "permute_ty pi (TConst i) = TConst (pi \<bullet> i)"
| "permute_ty pi (TApp A M) = TApp (permute_ty pi A) (permute_trm pi M)"
| "permute_ty pi (TPi A x B) = TPi (permute_ty pi A) (pi \<bullet> x) (permute_ty pi B)"
| "permute_trm pi (Const i) = Const (pi \<bullet> i)"
| "permute_trm pi (Var x) = Var (pi \<bullet> x)"
| "permute_trm pi (App M N) = App (permute_trm pi M) (permute_trm pi N)"
| "permute_trm pi (Lam A x M) = Lam (permute_ty pi A) (pi \<bullet> x) (permute_trm pi M)"

lemma rperm_zero_ok: "0 \<bullet> (x :: kind) = x \<and> 0 \<bullet> (y :: ty) = y \<and> 0 \<bullet> (z :: trm) = z"
apply(induct_tac rule: kind_ty_trm.induct)
apply(simp_all)
done
instance
apply default
apply (simp_all only:rperm_zero_ok)
apply(induct_tac[!] x)
apply(simp_all)
apply(induct_tac ty)
apply(simp_all)
apply(induct_tac trm)
apply(simp_all)
apply(induct_tac trm)
apply(simp_all)
done

end

inductive
    akind :: "kind \<Rightarrow> kind \<Rightarrow> bool" ("_ \<approx>ki _" [100, 100] 100)
and aty   :: "ty \<Rightarrow> ty \<Rightarrow> bool"     ("_ \<approx>ty _" [100, 100] 100)
and atrm  :: "trm \<Rightarrow> trm \<Rightarrow> bool"   ("_ \<approx>tr _" [100, 100] 100)
where
  a1: "(Type) \<approx>ki (Type)"
| a2: "\<lbrakk>A \<approx>ty A'; \<exists>pi. (rfv_kind K - {atom x} = rfv_kind K' - {atom x'} \<and> (rfv_kind K - {atom x})\<sharp>* pi \<and> (pi \<bullet> K) \<approx>ki K' \<and> (pi \<bullet> x) = x')\<rbrakk> \<Longrightarrow> (KPi A x K) \<approx>ki (KPi A' x' K')"
| a3: "i = j \<Longrightarrow> (TConst i) \<approx>ty (TConst j)"
| a4: "\<lbrakk>A \<approx>ty A'; M \<approx>tr M'\<rbrakk> \<Longrightarrow> (TApp A M) \<approx>ty (TApp A' M')"
| a5: "\<lbrakk>A \<approx>ty A'; \<exists>pi. (rfv_ty B - {atom x} = rfv_ty B' - {atom x'} \<and> (rfv_ty B - {atom x})\<sharp>* pi \<and> (pi \<bullet> B) \<approx>ty B' \<and> (pi \<bullet> x) = x')\<rbrakk> \<Longrightarrow> (TPi A x B) \<approx>ty (TPi A' x' B')"
| a6: "i = j \<Longrightarrow> (Const i) \<approx>tr (Const j)"
| a7: "x = y \<Longrightarrow> (Var x) \<approx>tr (Var y)"
| a8: "\<lbrakk>M \<approx>tr M'; N \<approx>tr N'\<rbrakk> \<Longrightarrow> (App M N) \<approx>tr (App M' N')"
| a9: "\<lbrakk>A \<approx>ty A'; \<exists>pi. (rfv_trm M - {atom x} = rfv_trm M' - {atom x'} \<and> (rfv_trm M - {atom x})\<sharp>* pi \<and> (pi \<bullet> M) \<approx>tr M' \<and> (pi \<bullet> x) = x')\<rbrakk> \<Longrightarrow> (Lam A x M) \<approx>tr (Lam A' x' M')"

(*
function(sequential)
    akind :: "kind \<Rightarrow> kind \<Rightarrow> bool" ("_ \<approx>ki _" [100, 100] 100)
and aty   :: "ty \<Rightarrow> ty \<Rightarrow> bool"     ("_ \<approx>ty _" [100, 100] 100)
and atrm  :: "trm \<Rightarrow> trm \<Rightarrow> bool"   ("_ \<approx>tr _" [100, 100] 100)
where
  a1: "(Type) \<approx>ki (Type) = True"
| a2: "(KPi A x K) \<approx>ki (KPi A' x' K') = (A \<approx>ty A' \<and> (\<exists>pi. (rfv_kind K - {atom x} = rfv_kind K' - {atom x'} \<and> (rfv_kind K - {atom x})\<sharp>* pi \<and> (pi \<bullet> K) \<approx>ki K' \<and> (pi \<bullet> x) = x')))"
| "_ \<approx>ki _ = False"
| a3: "(TConst i) \<approx>ty (TConst j) = (i = j)"
| a4: "(TApp A M) \<approx>ty (TApp A' M') = (A \<approx>ty A' \<and> M \<approx>tr M')"
| a5: "(TPi A x B) \<approx>ty (TPi A' x' B') = ((A \<approx>ty A') \<and> (\<exists>pi. rfv_ty B - {atom x} = rfv_ty B' - {atom x'} \<and> (rfv_ty B - {atom x})\<sharp>* pi \<and> (pi \<bullet> B) \<approx>ty B' \<and> (pi \<bullet> x) = x'))"
| "_ \<approx>ty _ = False"
| a6: "(Const i) \<approx>tr (Const j) = (i = j)"
| a7: "(Var x) \<approx>tr (Var y) = (x = y)"
| a8: "(App M N) \<approx>tr (App M' N') = (M \<approx>tr M' \<and> N \<approx>tr N')"
| a9: "(Lam A x M) \<approx>tr (Lam A' x' M') = (A \<approx>ty A' \<and> (\<exists>pi. rfv_trm M - {atom x} = rfv_trm M' - {atom x'} \<and> (rfv_trm M - {atom x})\<sharp>* pi \<and> (pi \<bullet> M) \<approx>tr M' \<and> (pi \<bullet> x) = x'))"
| "_ \<approx>tr _ = False"
apply (pat_completeness)
apply simp_all
done
termination
by (size_change)
*)

lemma akind_aty_artm_inj:
  "(Type) \<approx>ki (Type) = True"
  "(KPi A x K) \<approx>ki (KPi A' x' K') = (A \<approx>ty A' \<and> (\<exists>pi. (rfv_kind K - {atom x} = rfv_kind K' - {atom x'} \<and> (rfv_kind K - {atom x})\<sharp>* pi \<and> (pi \<bullet> K) \<approx>ki K' \<and> (pi \<bullet> x) = x')))"
  "(TConst i) \<approx>ty (TConst j) = (i = j)"
  "(TApp A M) \<approx>ty (TApp A' M') = (A \<approx>ty A' \<and> M \<approx>tr M')"
  "(TPi A x B) \<approx>ty (TPi A' x' B') = ((A \<approx>ty A') \<and> (\<exists>pi. rfv_ty B - {atom x} = rfv_ty B' - {atom x'} \<and> (rfv_ty B - {atom x})\<sharp>* pi \<and> (pi \<bullet> B) \<approx>ty B' \<and> (pi \<bullet> x) = x'))"
  "(Const i) \<approx>tr (Const j) = (i = j)"
  "(Var x) \<approx>tr (Var y) = (x = y)"
  "(App M N) \<approx>tr (App M' N') = (M \<approx>tr M' \<and> N \<approx>tr N')"
  "(Lam A x M) \<approx>tr (Lam A' x' M') = (A \<approx>ty A' \<and> (\<exists>pi. rfv_trm M - {atom x} = rfv_trm M' - {atom x'} \<and> (rfv_trm M - {atom x})\<sharp>* pi \<and> (pi \<bullet> M) \<approx>tr M' \<and> (pi \<bullet> x) = x'))"
apply -
apply (simp add: akind_aty_atrm.intros)

apply rule apply (erule akind.cases) apply simp apply blast
apply (simp only: akind_aty_atrm.intros)

apply rule apply (erule aty.cases) apply simp apply simp apply simp
apply (simp only: akind_aty_atrm.intros)

apply rule apply (erule aty.cases) apply simp apply simp apply simp
apply (simp only: akind_aty_atrm.intros)

apply rule apply (erule aty.cases) apply simp apply simp apply blast
apply (simp only: akind_aty_atrm.intros)

apply rule apply (erule atrm.cases) apply simp apply simp apply simp apply blast
apply (simp only: akind_aty_atrm.intros)

apply rule apply (erule atrm.cases) apply simp apply simp apply simp apply blast
apply (simp only: akind_aty_atrm.intros)

apply rule apply (erule atrm.cases) apply simp apply simp apply simp apply blast
apply (simp only: akind_aty_atrm.intros)

apply rule apply (erule atrm.cases) apply simp apply simp apply simp apply blast
apply (simp only: akind_aty_atrm.intros)
done

(* TODO: ask Stefan why 'induct' goes wrong, commented out commands should work *)

lemma rfv_eqvt[eqvt]:
  "((pi\<bullet>rfv_kind t1) = rfv_kind (pi\<bullet>t1))"
  "((pi\<bullet>rfv_ty t2) = rfv_ty (pi\<bullet>t2))"
  "((pi\<bullet>rfv_trm t3) = rfv_trm (pi\<bullet>t3))"
apply(induct t1 and t2 and t3 rule: kind_ty_trm.inducts)
apply(simp_all add:  union_eqvt Diff_eqvt)
apply(simp_all add: permute_set_eq atom_eqvt)
done

lemma alpha_eqvt:
  "t1 \<approx>ki s1 \<Longrightarrow> (pi \<bullet> t1) \<approx>ki (pi \<bullet> s1)"
  "t2 \<approx>ty s2 \<Longrightarrow> (pi \<bullet> t2) \<approx>ty (pi \<bullet> s2)"
  "t3 \<approx>tr s3 \<Longrightarrow> (pi \<bullet> t3) \<approx>tr (pi \<bullet> s3)"
apply(induct rule: akind_aty_atrm.inducts)
apply (simp_all add: akind_aty_atrm.intros)
apply(rule a2)
apply simp
apply(erule conjE)
apply(erule exE)
apply(erule conjE)
apply(rule_tac x="pi \<bullet> pia" in exI)
apply(rule conjI)
apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1])
apply(simp add: eqvts atom_eqvt)
apply(rule conjI)
apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])
apply(simp add: eqvts atom_eqvt)
apply(simp add: permute_eqvt[symmetric])
apply(rule a5)
apply simp
apply(erule conjE)
apply(erule exE)
apply(erule conjE)
apply(rule_tac x="pi \<bullet> pia" in exI)
apply(rule conjI)
apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1])
apply(simp add: eqvts atom_eqvt)
apply(rule conjI)
apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])
apply(simp add: eqvts atom_eqvt)
apply(simp add: permute_eqvt[symmetric])
apply(rule a9)
apply simp
apply(erule conjE)
apply(erule exE)
apply(erule conjE)
apply(rule_tac x="pi \<bullet> pia" in exI)
apply(rule conjI)
apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1])
apply(simp add: eqvts atom_eqvt)
apply(rule conjI)
apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])
apply(simp add: eqvts atom_eqvt)
apply(simp add: permute_eqvt[symmetric])
done

lemma al_refl:
  fixes K::"kind" 
  and   A::"ty"
  and   M::"trm"
  shows "K \<approx>ki K"
  and   "A \<approx>ty A"
  and   "M \<approx>tr M"
  apply(induct K and A and M rule: kind_ty_trm.inducts)
  apply(auto intro: akind_aty_atrm.intros)
  apply (rule a2)
  apply auto
  apply(rule_tac x="0" in exI)
  apply(simp_all add: fresh_star_def fresh_zero_perm)
  apply (rule a5)
  apply auto
  apply(rule_tac x="0" in exI)
  apply(simp_all add: fresh_star_def fresh_zero_perm)
  apply (rule a9)
  apply auto
  apply(rule_tac x="0" in exI)
  apply(simp_all add: fresh_star_def fresh_zero_perm)
  done

lemma alpha_equivps:
  shows "equivp akind"
  and   "equivp aty"
  and   "equivp atrm"
sorry

quotient_type KIND = kind / akind
  by (rule alpha_equivps)

quotient_type
    TY = ty / aty and
    TRM = trm / atrm
  by (auto intro: alpha_equivps)

quotient_definition
   "TYP :: KIND"
as
  "Type"

quotient_definition
   "KPI :: TY \<Rightarrow> name \<Rightarrow> KIND \<Rightarrow> KIND"
as
  "KPi"

quotient_definition
   "TCONST :: ident \<Rightarrow> TY"
as
  "TConst"

quotient_definition
   "TAPP :: TY \<Rightarrow> TRM \<Rightarrow> TY"
as
  "TApp"

quotient_definition
   "TPI :: TY \<Rightarrow> name \<Rightarrow> TY \<Rightarrow> TY"
as
  "TPi"

(* FIXME: does not work with CONST *)
quotient_definition
   "CONS :: ident \<Rightarrow> TRM"
as
  "Const"

quotient_definition
   "VAR :: name \<Rightarrow> TRM"
as
  "Var"

quotient_definition
   "APP :: TRM \<Rightarrow> TRM \<Rightarrow> TRM"
as
  "App"

quotient_definition
   "LAM :: TY \<Rightarrow> name \<Rightarrow> TRM \<Rightarrow> TRM"
as
  "Lam"

(* FIXME: print out a warning if the type contains a liftet type, like kind \<Rightarrow> name set *)
quotient_definition
   "fv_kind :: KIND \<Rightarrow> atom set"
as
  "rfv_kind"

quotient_definition
   "fv_ty :: TY \<Rightarrow> atom set"
as
  "rfv_ty"

quotient_definition
   "fv_trm :: TRM \<Rightarrow> atom set"
as
  "rfv_trm"

lemma alpha_rfv:
  shows "(t \<approx>ki s \<longrightarrow> rfv_kind t = rfv_kind s) \<and>
     (t1 \<approx>ty s1 \<longrightarrow> rfv_ty t1 = rfv_ty s1) \<and>
     (t2 \<approx>tr s2 \<longrightarrow> rfv_trm t2 = rfv_trm s2)"
  apply(rule akind_aty_atrm.induct)
  apply(simp_all)
  done

lemma perm_rsp[quot_respect]:
  "(op = ===> akind ===> akind) permute permute"
  "(op = ===> aty ===> aty) permute permute"
  "(op = ===> atrm ===> atrm) permute permute"
  by (simp_all add:alpha_eqvt)

lemma tconst_rsp[quot_respect]: 
  "(op = ===> aty) TConst TConst"
  apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done
lemma tapp_rsp[quot_respect]: 
  "(aty ===> atrm ===> aty) TApp TApp" 
  apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done
lemma var_rsp[quot_respect]: 
  "(op = ===> atrm) Var Var"
  apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done
lemma app_rsp[quot_respect]: 
  "(atrm ===> atrm ===> atrm) App App"
  apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done
lemma const_rsp[quot_respect]: 
  "(op = ===> atrm) Const Const"
  apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done

lemma kpi_rsp[quot_respect]: 
  "(aty ===> op = ===> akind ===> akind) KPi KPi"
  apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9)
  apply (rule a2) apply simp
  apply (rule_tac x="0" in exI)
  apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv)
  done

lemma tpi_rsp[quot_respect]: 
  "(aty ===> op = ===> aty ===> aty) TPi TPi"
  apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9)
  apply (rule a5) apply simp
  apply (rule_tac x="0" in exI)
  apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv)
  done
lemma lam_rsp[quot_respect]: 
  "(aty ===> op = ===> atrm ===> atrm) Lam Lam"
  apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9)
  apply (rule a9) apply simp
  apply (rule_tac x="0" in exI)
  apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv)
  done

lemma rfv_ty_rsp[quot_respect]: 
  "(aty ===> op =) rfv_ty rfv_ty"
  by (simp add: alpha_rfv)
lemma rfv_kind_rsp[quot_respect]:
  "(akind ===> op =) rfv_kind rfv_kind"
  by (simp add: alpha_rfv)
lemma rfv_trm_rsp[quot_respect]:
  "(atrm ===> op =) rfv_trm rfv_trm"
  by (simp add: alpha_rfv)

lemma KIND_TY_TRM_induct: "\<lbrakk>P10 TYP; \<And>ty name kind. \<lbrakk>P20 ty; P10 kind\<rbrakk> \<Longrightarrow> P10 (KPI ty name kind); \<And>ident. P20 (TCONST ident);
 \<And>ty trm. \<lbrakk>P20 ty; P30 trm\<rbrakk> \<Longrightarrow> P20 (TAPP ty trm);
 \<And>ty1 name ty2. \<lbrakk>P20 ty1; P20 ty2\<rbrakk> \<Longrightarrow> P20 (TPI ty1 name ty2); \<And>ident. P30 (CONS ident);
 \<And>name. P30 (VAR name); \<And>trm1 trm2. \<lbrakk>P30 trm1; P30 trm2\<rbrakk> \<Longrightarrow> P30 (APP trm1 trm2);
 \<And>ty name trm. \<lbrakk>P20 ty; P30 trm\<rbrakk> \<Longrightarrow> P30 (LAM ty name trm)\<rbrakk>
\<Longrightarrow> P10 kind \<and> P20 ty \<and> P30 trm"
by (lifting kind_ty_trm.induct)

instantiation KIND and TY and TRM :: pt
begin

quotient_definition
  "permute_KIND :: perm \<Rightarrow> KIND \<Rightarrow> KIND"
as
  "permute :: perm \<Rightarrow> kind \<Rightarrow> kind"

quotient_definition
  "permute_TY :: perm \<Rightarrow> TY \<Rightarrow> TY"
as
  "permute :: perm \<Rightarrow> ty \<Rightarrow> ty"

quotient_definition
  "permute_TRM :: perm \<Rightarrow> TRM \<Rightarrow> TRM"
as
  "permute :: perm \<Rightarrow> trm \<Rightarrow> trm"

term "permute_TRM"
thm permute_kind_permute_ty_permute_trm.simps
lemma [simp]:
shows "pi \<bullet> TYP = TYP"
and   "pi \<bullet> (KPI t n k) = KPI (pi \<bullet> t) (pi \<bullet> n) (pi \<bullet> k)"
and   "pi \<bullet> (TCONST i) = TCONST (pi \<bullet> i)"
and   "pi \<bullet> (TAPP A M) = TAPP (pi \<bullet> A) (pi \<bullet> M)"
and   "pi \<bullet> (TPI A x B) = TPI (pi \<bullet> A) (pi \<bullet> x) (pi \<bullet> B)"
and   "pi \<bullet> (CONS i) = CONS (pi \<bullet> i)"
and   "pi \<bullet> (VAR x) = VAR (pi \<bullet> x)"
and   "pi \<bullet> (APP M N) = APP (pi \<bullet> M) (pi \<bullet> N)"
and   "pi \<bullet> (LAM A x M) = LAM (pi \<bullet> A) (pi \<bullet> x) (pi \<bullet> M)"
apply (lifting permute_kind_permute_ty_permute_trm.simps)
done

lemma perm_zero_ok: "0 \<bullet> (x :: KIND) = x \<and> 0 \<bullet> (y :: TY) = y \<and> 0 \<bullet> (z :: TRM) = z"
apply (induct rule: KIND_TY_TRM_induct)
apply simp_all
done

lemma perm_add_ok: "((p1 + q1) \<bullet> (x1 :: KIND) = (p1 \<bullet> q1 \<bullet> (x1 :: KIND))) \<and> ((p2 + q2) \<bullet> (x2 :: TY) = p2 \<bullet> q2 \<bullet> x2) \<and> ((p3 + q3) \<bullet> (x3 :: TRM) = p3 \<bullet> q3 \<bullet> x3)"
apply(rule KIND_TY_TRM_induct[of 
"\<lambda>x1. ((p1 + q1) \<bullet> (x1 :: KIND) = (p1 \<bullet> q1 \<bullet> x1))"
"\<lambda>x2. ((p2 + q2) \<bullet> (x2 :: TY) = p2 \<bullet> q2 \<bullet> x2)"
"\<lambda>x3. ((p3 + q3) \<bullet> (x3 :: TRM) = p3 \<bullet> q3 \<bullet> x3)"])
apply (simp_all)
sorry

instance
apply default
apply (simp_all add: perm_zero_ok perm_add_ok)
done

end

lemma "\<lbrakk>P10 TYP TYP;
 \<And>A A' K x K' x'.
    \<lbrakk>(A :: TY) = A'; P20 A A';
     \<exists>pi. fv_kind K - {atom x} = fv_kind K' - {atom x'} \<and>
          (fv_kind K - {atom x}) \<sharp>* pi \<and> ((pi \<bullet> K) = K' \<and> P10 (pi \<bullet> K) K') \<and> pi \<bullet> x = x'\<rbrakk>
    \<Longrightarrow> P10 (KPI A x K) (KPI A' x' K');
 \<And>i j. i = j \<Longrightarrow> P20 (TCONST i) (TCONST j);
 \<And>A A' M M'. \<lbrakk>A = A'; P20 A A'; M = M'; P30 M M'\<rbrakk> \<Longrightarrow> P20 (TAPP A M) (TAPP A' M');
 \<And>A A' B x B' x'.
    \<lbrakk>A = A'; P20 A A';
     \<exists>pi. fv_ty B - {atom x} = fv_ty B' - {atom x'} \<and>
          (fv_ty B - {atom x}) \<sharp>* pi \<and> ((pi \<bullet> B) = B' \<and> P20 (pi \<bullet> B) B') \<and> pi \<bullet> x = x'\<rbrakk>
    \<Longrightarrow> P20 (TPI A x B) (TPI A' x' B');
 \<And>i j. i = j \<Longrightarrow> P30 (CONS i) (CONS j); \<And>x y. x = y \<Longrightarrow> P30 (VAR x) (VAR y);
 \<And>M M' N N'. \<lbrakk>M = M'; P30 M M'; N = N'; P30 N N'\<rbrakk> \<Longrightarrow> P30 (APP M N) (APP M' N');
 \<And>A A' M x M' x'.
    \<lbrakk>A = A'; P20 A A';
     \<exists>pi. fv_trm M - {atom x} = fv_trm M' - {atom x'} \<and>
          (fv_trm M - {atom x}) \<sharp>* pi \<and> ((pi \<bullet> M) = M' \<and> P30 (pi \<bullet> M) M') \<and> pi \<bullet> x = x'\<rbrakk>
    \<Longrightarrow> P30 (LAM A x M) (LAM A' x' M')\<rbrakk>
\<Longrightarrow> (x10 = x20 \<longrightarrow> P10 x10 x20) \<and>
   (x30 = x40 \<longrightarrow> P20 x30 x40) \<and> (x50 = x60 \<longrightarrow> P30 x50 x60)"
apply (lifting akind_aty_atrm.induct)
done

end