Theory Class3

theory Class3
  imports Class2
begin

text ‹3rd Main Lemma›

lemma Cut_a_redu_elim:
  assumes a: "Cut <a>.M (x).N ⟶⇩a R"
  shows "(∃M'. R = Cut <a>.M' (x).N ∧ M ⟶⇩a M') ∨
         (∃N'. R = Cut <a>.M (x).N' ∧ N ⟶⇩a N') ∨
         (Cut <a>.M (x).N ⟶⇩c R) ∨
         (Cut <a>.M (x).N ⟶⇩l R)"
  using a
  apply(erule_tac a_redu.cases)
                  apply(simp_all)
   apply(simp_all add: trm.inject)
   apply(rule disjI1)
   apply(auto simp add: alpha)[1]
    apply(rule_tac x="[(a,aa)]∙M'" in exI)
    apply(perm_simp add: fresh_left calc_atm a_redu.eqvt fresh_a_redu)
   apply(rule_tac x="[(a,aa)]∙M'" in exI)
   apply(perm_simp add: fresh_left calc_atm a_redu.eqvt fresh_a_redu)
  apply(rule disjI2)
  apply(rule disjI1)
  apply(auto simp add: alpha)[1]
   apply(rule_tac x="[(x,xa)]∙N'" in exI)
   apply(perm_simp add: fresh_left calc_atm a_redu.eqvt fresh_a_redu)
  apply(rule_tac x="[(x,xa)]∙N'" in exI)
  apply(perm_simp add: fresh_left calc_atm a_redu.eqvt fresh_a_redu)
  done

lemma Cut_c_redu_elim:
  assumes a: "Cut <a>.M (x).N ⟶⇩c R"
  shows "(R = M{a:=(x).N} ∧ ¬fic M a) ∨
         (R = N{x:=<a>.M} ∧ ¬fin N x)"
  using a
  apply(erule_tac c_redu.cases)
   apply(simp_all)
   apply(simp_all add: trm.inject)
   apply(rule disjI1)
   apply(auto simp add: alpha)[1]
       apply(simp add: subst_rename fresh_atm)
      apply(simp add: subst_rename fresh_atm)
     apply(drule_tac pi="[(a,aa)]" in fic.eqvt(2))
     apply(perm_simp)
    apply(simp add: subst_rename fresh_atm fresh_prod)
   apply(drule_tac pi="[(a,aa)]" in fic.eqvt(2))
   apply(perm_simp)
  apply(rule disjI2)
  apply(auto simp add: alpha)[1]
      apply(simp add: subst_rename fresh_atm)
     apply(drule_tac pi="[(x,xa)]" in fin.eqvt(1))
     apply(perm_simp)
    apply(simp add: subst_rename fresh_atm fresh_prod)
   apply(simp add: subst_rename fresh_atm fresh_prod)
  apply(drule_tac pi="[(x,xa)]" in fin.eqvt(1))
  apply(perm_simp)
  done

lemma not_fic_crename_aux:
  assumes a: "fic M c" "c♯(a,b)"
  shows "fic (M[a⊢c>b]) c" 
  using a
  apply(nominal_induct M avoiding: c a b rule: trm.strong_induct)
             apply(auto dest!: fic_elims intro!: fic.intros simp add: fresh_prod fresh_atm rename_fresh abs_fresh)
  done

lemma not_fic_crename:
  assumes a: "¬(fic (M[a⊢c>b]) c)" "c♯(a,b)"
  shows "¬(fic M c)" 
  using a
  apply(auto dest:  not_fic_crename_aux)
  done

lemma not_fin_crename_aux:
  assumes a: "fin M y"
  shows "fin (M[a⊢c>b]) y" 
  using a
  apply(nominal_induct M avoiding: a b rule: trm.strong_induct)
             apply(auto dest!: fin_elims intro!: fin.intros simp add: fresh_prod fresh_atm rename_fresh abs_fresh)
  done

lemma not_fin_crename:
  assumes a: "¬(fin (M[a⊢c>b]) y)" 
  shows "¬(fin M y)" 
  using a
  apply(auto dest:  not_fin_crename_aux)
  done

lemma crename_fresh_interesting1:
  fixes c::"coname"
  assumes a: "c♯(M[a⊢c>b])" "c♯(a,b)"
  shows "c♯M"
  using a
  apply(nominal_induct M avoiding: c a b rule: trm.strong_induct)
             apply(auto split: if_splits simp add: abs_fresh)
  done

lemma crename_fresh_interesting2:
  fixes x::"name"
  assumes a: "x♯(M[a⊢c>b])" 
  shows "x♯M"
  using a
  apply(nominal_induct M avoiding: x a b rule: trm.strong_induct)
             apply(auto split: if_splits simp add: abs_fresh abs_supp fin_supp fresh_atm)
  done


lemma fic_crename:
  assumes a: "fic (M[a⊢c>b]) c" "c♯(a,b)"
  shows "fic M c" 
  using a
  apply(nominal_induct M avoiding: c a b rule: trm.strong_induct)
             apply(auto dest!: fic_elims intro!: fic.intros simp add: fresh_prod fresh_atm rename_fresh abs_fresh
      split: if_splits)
       apply(auto dest: crename_fresh_interesting1 simp add: fresh_prod fresh_atm)
  done

lemma fin_crename:
  assumes a: "fin (M[a⊢c>b]) x"
  shows "fin M x" 
  using a
  apply(nominal_induct M avoiding: x a b rule: trm.strong_induct)
             apply(auto dest!: fin_elims intro!: fin.intros simp add: fresh_prod fresh_atm rename_fresh abs_fresh
      split: if_splits)
        apply(auto dest: crename_fresh_interesting2 simp add: fresh_prod fresh_atm)
  done

lemma crename_Cut:
  assumes a: "R[a⊢c>b] = Cut <c>.M (x).N" "c♯(a,b,N,R)" "x♯(M,R)"
  shows "∃M' N'. R = Cut <c>.M' (x).N' ∧ M'[a⊢c>b] = M ∧ N'[a⊢c>b] = N ∧ c♯N' ∧ x♯M'"
  using a
  apply(nominal_induct R avoiding: a b c x M N rule: trm.strong_induct)
             apply(auto split: if_splits)
  apply(simp add: trm.inject)
  apply(auto simp add: alpha)
    apply(rule_tac x="[(name,x)]∙trm2" in exI)
    apply(perm_simp)
    apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
    apply(drule sym)
    apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
    apply(simp add: eqvts calc_atm)
   apply(rule_tac x="[(coname,c)]∙trm1" in exI)
   apply(perm_simp)
   apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
   apply(drule sym)
   apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
   apply(simp add: eqvts calc_atm)
   apply(auto simp add: fresh_atm)[1]
  apply(rule_tac x="[(coname,c)]∙trm1" in exI)
  apply(perm_simp)
  apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
  apply(rule_tac x="[(name,x)]∙trm2" in exI)
  apply(perm_simp)
  apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
  apply(drule sym)
  apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
  apply(simp add: eqvts calc_atm)
  apply(auto simp add: fresh_atm)[1]
   apply(drule sym)
   apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
   apply(simp add: eqvts calc_atm)
  apply(drule sym)
  apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
  apply(simp add: eqvts calc_atm)
  done

lemma crename_NotR:
  assumes a: "R[a⊢c>b] = NotR (x).N c" "x♯R" "c♯(a,b)"
  shows "∃N'. (R = NotR (x).N' c) ∧ N'[a⊢c>b] = N" 
  using a
  apply(nominal_induct R avoiding: a b c x N rule: trm.strong_induct)
             apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
  apply(rule_tac x="[(name,x)]∙trm" in exI)
  apply(perm_simp)
  apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
  apply(drule sym)
  apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
  apply(simp add: eqvts calc_atm)
  done

lemma crename_NotR':
  assumes a: "R[a⊢c>b] = NotR (x).N c" "x♯R" "c♯a"
  shows "(∃N'. (R = NotR (x).N' c) ∧ N'[a⊢c>b] = N) ∨ (∃N'. (R = NotR (x).N' a) ∧ b=c ∧ N'[a⊢c>b] = N)"
  using a
  apply(nominal_induct R avoiding: a b c x N rule: trm.strong_induct)
             apply(auto split: if_splits simp add: fresh_prod fresh_atm abs_fresh alpha trm.inject)
   apply(rule_tac x="[(name,x)]∙trm" in exI)
   apply(perm_simp)
   apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
   apply(drule sym)
   apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
   apply(simp add: eqvts calc_atm)
  apply(rule_tac x="[(name,x)]∙trm" in exI)
  apply(perm_simp)
  apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
  apply(drule sym)
  apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
  apply(simp add: eqvts calc_atm)
  done

lemma crename_NotR_aux:
  assumes a: "R[a⊢c>b] = NotR (x).N c" 
  shows "(a=c ∧ a=b) ∨ (a≠c)" 
  using a
  apply(nominal_induct R avoiding: a b c x N rule: trm.strong_induct)
             apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
  done

lemma crename_NotL:
  assumes a: "R[a⊢c>b] = NotL <c>.N y" "c♯(R,a,b)"
  shows "∃N'. (R = NotL <c>.N' y) ∧ N'[a⊢c>b] = N" 
  using a
  apply(nominal_induct R avoiding: a b c y N rule: trm.strong_induct)
             apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
  apply(rule_tac x="[(coname,c)]∙trm" in exI)
  apply(perm_simp)
  apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
  apply(drule sym)
  apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
  apply(simp add: eqvts calc_atm)
  done

lemma crename_AndL1:
  assumes a: "R[a⊢c>b] = AndL1 (x).N y" "x♯R"
  shows "∃N'. (R = AndL1 (x).N' y) ∧ N'[a⊢c>b] = N" 
  using a
  apply(nominal_induct R avoiding: a b x y N rule: trm.strong_induct)
             apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
  apply(rule_tac x="[(name1,x)]∙trm" in exI)
  apply(perm_simp)
  apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
  apply(drule sym)
  apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
  apply(simp add: eqvts calc_atm)
  done

lemma crename_AndL2:
  assumes a: "R[a⊢c>b] = AndL2 (x).N y" "x♯R"
  shows "∃N'. (R = AndL2 (x).N' y) ∧ N'[a⊢c>b] = N" 
  using a
  apply(nominal_induct R avoiding: a b x y N rule: trm.strong_induct)
             apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
  apply(rule_tac x="[(name1,x)]∙trm" in exI)
  apply(perm_simp)
  apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
  apply(drule sym)
  apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
  apply(simp add: eqvts calc_atm)
  done

lemma crename_AndR_aux:
  assumes a: "R[a⊢c>b] = AndR <c>.M <d>.N e" 
  shows "(a=e ∧ a=b) ∨ (a≠e)" 
  using a
  apply(nominal_induct R avoiding: a b c d e M N rule: trm.strong_induct)
             apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
  done

lemma crename_AndR:
  assumes a: "R[a⊢c>b] = AndR <c>.M <d>.N e" "c♯(a,b,d,e,N,R)" "d♯(a,b,c,e,M,R)" "e♯(a,b)"
  shows "∃M' N'. R = AndR <c>.M' <d>.N' e ∧ M'[a⊢c>b] = M ∧ N'[a⊢c>b] = N ∧ c♯N' ∧ d♯M'"
  using a
  apply(nominal_induct R avoiding: a b c d e M N rule: trm.strong_induct)
             apply(auto split: if_splits simp add: trm.inject alpha)
        apply(simp add: fresh_atm fresh_prod)
       apply(rule_tac x="[(coname2,d)]∙trm2" in exI)
       apply(perm_simp)
       apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
      apply(rule_tac x="[(coname1,c)]∙trm1" in exI)
      apply(perm_simp)
      apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
     apply(rule_tac x="[(coname1,c)]∙trm1" in exI)
     apply(perm_simp)
     apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
    apply(rule_tac x="[(coname2,d)]∙trm2" in exI)
    apply(perm_simp)
    apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
   apply(rule_tac x="[(coname1,c)]∙trm1" in exI)
   apply(perm_simp)
   apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
  apply(rule_tac x="[(coname1,c)]∙trm1" in exI)
  apply(perm_simp)
  apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
  apply(rule_tac x="[(coname2,d)]∙trm2" in exI)
  apply(perm_simp)
  apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
   apply(drule sym)
   apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
   apply(simp add: eqvts calc_atm)
  apply(drule_tac s="trm2[a⊢c>b]" in  sym)
  apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
  apply(simp add: eqvts calc_atm)
  done

lemma crename_AndR':
  assumes a: "R[a⊢c>b] = AndR <c>.M <d>.N e" "c♯(a,b,d,e,N,R)" "d♯(a,b,c,e,M,R)" "e♯a"
  shows "(∃M' N'. R = AndR <c>.M' <d>.N' e ∧ M'[a⊢c>b] = M ∧ N'[a⊢c>b] = N ∧ c♯N' ∧ d♯M') ∨
         (∃M' N'. R = AndR <c>.M' <d>.N' a ∧ b=e ∧ M'[a⊢c>b] = M ∧ N'[a⊢c>b] = N ∧ c♯N' ∧ d♯M')"
  using a [[simproc del: defined_all]]
  apply(nominal_induct R avoiding: a b c d e M N rule: trm.strong_induct)
             apply(auto split: if_splits simp add: trm.inject alpha)[1]
            apply(auto split: if_splits simp add: trm.inject alpha)[1]
           apply(auto split: if_splits simp add: trm.inject alpha)[1]
          apply(auto split: if_splits simp add: trm.inject alpha)[1]
         apply(simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm trm.inject alpha)[1]
         apply(case_tac "coname3=a")
          apply(simp)
          apply(rule_tac x="[(coname1,c)]∙trm1" in exI)
          apply(perm_simp)
          apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
          apply(rule_tac x="[(coname2,d)]∙trm2" in exI)
          apply(perm_simp)
          apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm trm.inject alpha split: if_splits)[1]
           apply(drule sym)
           apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
           apply(simp add: eqvts calc_atm)
          apply(drule_tac s="trm2[a⊢c>e]" in  sym)
          apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
          apply(simp add: eqvts calc_atm)
         apply(simp)
         apply(rule_tac x="[(coname1,c)]∙trm1" in exI)
         apply(perm_simp)
         apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
         apply(rule_tac x="[(coname2,d)]∙trm2" in exI)
         apply(perm_simp)
         apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm trm.inject alpha split: if_splits)[1]
          apply(drule sym)
          apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
          apply(simp add: eqvts calc_atm)
         apply(drule_tac s="trm2[a⊢c>b]" in  sym)
         apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
         apply(simp add: eqvts calc_atm)
        apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
  done

lemma crename_OrR1_aux:
  assumes a: "R[a⊢c>b] = OrR1 <c>.M e" 
  shows "(a=e ∧ a=b) ∨ (a≠e)" 
  using a
  apply(nominal_induct R avoiding: a b c e M rule: trm.strong_induct)
             apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
  done

lemma crename_OrR1:
  assumes a: "R[a⊢c>b] = OrR1 <c>.N d" "c♯(R,a,b)" "d♯(a,b)"
  shows "∃N'. (R = OrR1 <c>.N' d) ∧ N'[a⊢c>b] = N" 
  using a
  apply(nominal_induct R avoiding: a b c d N rule: trm.strong_induct)
             apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
  apply(rule_tac x="[(coname1,c)]∙trm" in exI)
  apply(perm_simp)
  apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
  apply(drule sym)
  apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
  apply(simp add: eqvts calc_atm)
  done

lemma crename_OrR1':
  assumes a: "R[a⊢c>b] = OrR1 <c>.N d" "c♯(R,a,b)" "d♯a"
  shows "(∃N'. (R = OrR1 <c>.N' d) ∧ N'[a⊢c>b] = N) ∨
         (∃N'. (R = OrR1 <c>.N' a) ∧ b=d ∧ N'[a⊢c>b] = N)" 
  using a
  apply(nominal_induct R avoiding: a b c d N rule: trm.strong_induct)
             apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
   apply(rule_tac x="[(coname1,c)]∙trm" in exI)
   apply(perm_simp)
   apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
   apply(drule sym)
   apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
   apply(simp add: eqvts calc_atm)
  apply(rule_tac x="[(coname1,c)]∙trm" in exI)
  apply(perm_simp)
  apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
  apply(drule sym)
  apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
  apply(simp add: eqvts calc_atm)
  done

lemma crename_OrR2_aux:
  assumes a: "R[a⊢c>b] = OrR2 <c>.M e" 
  shows "(a=e ∧ a=b) ∨ (a≠e)" 
  using a
  apply(nominal_induct R avoiding: a b c e M rule: trm.strong_induct)
             apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
  done

lemma crename_OrR2:
  assumes a: "R[a⊢c>b] = OrR2 <c>.N d" "c♯(R,a,b)" "d♯(a,b)"
  shows "∃N'. (R = OrR2 <c>.N' d) ∧ N'[a⊢c>b] = N" 
  using a
  apply(nominal_induct R avoiding: a b c d N rule: trm.strong_induct)
             apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
  apply(rule_tac x="[(coname1,c)]∙trm" in exI)
  apply(perm_simp)
  apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
  apply(drule sym)
  apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
  apply(simp add: eqvts calc_atm)
  done

lemma crename_OrR2':
  assumes a: "R[a⊢c>b] = OrR2 <c>.N d" "c♯(R,a,b)" "d♯a"
  shows "(∃N'. (R = OrR2 <c>.N' d) ∧ N'[a⊢c>b] = N) ∨
         (∃N'. (R = OrR2 <c>.N' a) ∧ b=d ∧ N'[a⊢c>b] = N)" 
  using a
  apply(nominal_induct R avoiding: a b c d N rule: trm.strong_induct)
             apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
   apply(rule_tac x="[(coname1,c)]∙trm" in exI)
   apply(perm_simp)
   apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
   apply(drule sym)
   apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
   apply(simp add: eqvts calc_atm)
  apply(rule_tac x="[(coname1,c)]∙trm" in exI)
  apply(perm_simp)
  apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
  apply(drule sym)
  apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
  apply(simp add: eqvts calc_atm)
  done

lemma crename_OrL:
  assumes a: "R[a⊢c>b] = OrL (x).M (y).N z" "x♯(y,z,N,R)" "y♯(x,z,M,R)"
  shows "∃M' N'. R = OrL (x).M' (y).N' z ∧ M'[a⊢c>b] = M ∧ N'[a⊢c>b] = N ∧ x♯N' ∧ y♯M'"
  using a
  apply(nominal_induct R avoiding: a b x y z M N rule: trm.strong_induct)
             apply(auto split: if_splits simp add: trm.inject alpha)
    apply(rule_tac x="[(name2,y)]∙trm2" in exI)
    apply(perm_simp)
    apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
   apply(rule_tac x="[(name1,x)]∙trm1" in exI)
   apply(perm_simp)
   apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
  apply(rule_tac x="[(name1,x)]∙trm1" in exI)
  apply(perm_simp)
  apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
  apply(rule_tac x="[(name2,y)]∙trm2" in exI)
  apply(perm_simp)
  apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
   apply(drule sym)
   apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
   apply(simp add: eqvts calc_atm)
  apply(drule_tac s="trm2[a⊢c>b]" in  sym)
  apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
  apply(simp add: eqvts calc_atm)
  done

lemma crename_ImpL:
  assumes a: "R[a⊢c>b] = ImpL <c>.M (y).N z" "c♯(a,b,N,R)" "y♯(z,M,R)"
  shows "∃M' N'. R = ImpL <c>.M' (y).N' z ∧ M'[a⊢c>b] = M ∧ N'[a⊢c>b] = N ∧ c♯N' ∧ y♯M'"
  using a
  apply(nominal_induct R avoiding: a b c y z M N rule: trm.strong_induct)
             apply(auto split: if_splits simp add: trm.inject alpha)
    apply(rule_tac x="[(name1,y)]∙trm2" in exI)
    apply(perm_simp)
    apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
   apply(rule_tac x="[(coname,c)]∙trm1" in exI)
   apply(perm_simp)
   apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
  apply(rule_tac x="[(coname,c)]∙trm1" in exI)
  apply(perm_simp)
  apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
  apply(rule_tac x="[(name1,y)]∙trm2" in exI)
  apply(perm_simp)
  apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
   apply(drule sym)
   apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
   apply(simp add: eqvts calc_atm)
  apply(drule_tac s="trm2[a⊢c>b]" in  sym)
  apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
  apply(simp add: eqvts calc_atm)
  done

lemma crename_ImpR_aux:
  assumes a: "R[a⊢c>b] = ImpR (x).<c>.M e" 
  shows "(a=e ∧ a=b) ∨ (a≠e)" 
  using a
  apply(nominal_induct R avoiding: x a b c e M rule: trm.strong_induct)
             apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
  done

lemma crename_ImpR:
  assumes a: "R[a⊢c>b] = ImpR (x).<c>.N d" "c♯(R,a,b)" "d♯(a,b)" "x♯R" 
  shows "∃N'. (R = ImpR (x).<c>.N' d) ∧ N'[a⊢c>b] = N" 
  using a
  apply(nominal_induct R avoiding: a b x c d N rule: trm.strong_induct)
             apply(auto split: if_splits simp add: fresh_prod fresh_atm abs_perm alpha abs_fresh trm.inject)
   apply(rule_tac x="[(name,x)]∙trm" in exI)
   apply(perm_simp)
  apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
  apply(rule_tac x="[(name,x)]∙[(coname1, c)]∙trm" in exI)
  apply(perm_simp)
  apply(simp add: abs_supp fin_supp abs_fresh fresh_left calc_atm fresh_prod)
  apply(drule sym)
  apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
  apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
  apply(simp add: eqvts calc_atm)
  done

lemma crename_ImpR':
  assumes a: "R[a⊢c>b] = ImpR (x).<c>.N d" "c♯(R,a,b)" "x♯R" "d♯a"
  shows "(∃N'. (R = ImpR (x).<c>.N' d) ∧ N'[a⊢c>b] = N) ∨
         (∃N'. (R = ImpR (x).<c>.N' a) ∧ b=d ∧ N'[a⊢c>b] = N)" 
  using a
  apply(nominal_induct R avoiding: x a b c d N rule: trm.strong_induct)
             apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject abs_perm calc_atm)
   apply(rule_tac x="[(name,x)]∙[(coname1,c)]∙trm" in exI)
   apply(perm_simp)
   apply(simp add: abs_fresh fresh_left calc_atm fresh_prod abs_supp fin_supp)
   apply(drule sym)
   apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
   apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
   apply(simp add: eqvts calc_atm)
  apply(rule_tac x="[(name,x)]∙[(coname1,c)]∙trm" in exI)
  apply(perm_simp)
  apply(simp add: abs_fresh fresh_left calc_atm fresh_prod abs_supp fin_supp)
  apply(drule sym)
  apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
  apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
  apply(simp add: eqvts calc_atm)
  done

lemma crename_ax2:
  assumes a: "N[a⊢c>b] = Ax x c"
  shows "∃d. N = Ax x d"
  using a
  apply(nominal_induct N avoiding: a b rule: trm.strong_induct)
             apply(auto split: if_splits)
  apply(simp add: trm.inject)
  done

lemma crename_interesting1:
  assumes a: "distinct [a,b,c]"
  shows "M[a⊢c>c][c⊢c>b] = M[c⊢c>b][a⊢c>b]"
  using a
  apply(nominal_induct M avoiding: a c b rule: trm.strong_induct)
             apply(auto simp add: rename_fresh simp add: trm.inject alpha)
     apply(blast)
    apply(rotate_tac 12)
    apply(drule_tac x="a" in meta_spec)
    apply(rotate_tac 15)
    apply(drule_tac x="c" in meta_spec)
    apply(rotate_tac 15)
    apply(drule_tac x="b" in meta_spec)
    apply(blast)
   apply(blast)
  apply(blast)
  done

lemma crename_interesting2:
  assumes a: "a≠c" "a≠d" "a≠b" "c≠d" "b≠c"
  shows "M[a⊢c>b][c⊢c>d] = M[c⊢c>d][a⊢c>b]"
  using a
  apply(nominal_induct M avoiding: a c b d rule: trm.strong_induct)
             apply(auto simp add: rename_fresh simp add: trm.inject alpha)
  done

lemma crename_interesting3:
  shows "M[a⊢c>c][x⊢n>y] = M[x⊢n>y][a⊢c>c]"
  apply(nominal_induct M avoiding: a c x y rule: trm.strong_induct)
             apply(auto simp add: rename_fresh simp add: trm.inject alpha)
  done

lemma crename_credu:
  assumes a: "(M[a⊢c>b]) ⟶⇩c M'"
  shows "∃M0. M0[a⊢c>b]=M' ∧ M ⟶⇩c M0"
  using a
  apply(nominal_induct M≡"M[a⊢c>b]" M' avoiding: M a b rule: c_redu.strong_induct)
   apply(drule sym)
   apply(drule crename_Cut)
     apply(simp)
    apply(simp)
   apply(auto)
   apply(rule_tac x="M'{a:=(x).N'}" in exI)
   apply(rule conjI)
    apply(simp add: fresh_atm abs_fresh subst_comm fresh_prod)
   apply(rule c_redu.intros)
     apply(auto dest: not_fic_crename)[1]
    apply(simp add: abs_fresh)
   apply(simp add: abs_fresh)
  apply(drule sym)
  apply(drule crename_Cut)
    apply(simp)
   apply(simp)
  apply(auto)
  apply(rule_tac x="N'{x:=<a>.M'}" in exI)
  apply(rule conjI)
   apply(simp add: fresh_atm abs_fresh subst_comm fresh_prod)
  apply(rule c_redu.intros)
    apply(auto dest: not_fin_crename)[1]
   apply(simp add: abs_fresh)
  apply(simp add: abs_fresh)
  done

lemma crename_lredu:
  assumes a: "(M[a⊢c>b]) ⟶⇩l M'"
  shows "∃M0. M0[a⊢c>b]=M' ∧ M ⟶⇩l M0"
  using a
  apply(nominal_induct M≡"M[a⊢c>b]" M' avoiding: M a b rule: l_redu.strong_induct)
         apply(drule sym)
         apply(drule crename_Cut)
           apply(simp add: fresh_prod fresh_atm)
          apply(simp)
         apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
         apply(case_tac "aa=ba")
          apply(simp add: crename_id)
          apply(rule l_redu.intros)
            apply(simp)
           apply(simp add: fresh_atm)
          apply(assumption)
         apply(frule crename_ax2)
         apply(auto)[1]
         apply(case_tac "d=aa")
          apply(simp add: trm.inject)
          apply(rule_tac x="M'[a⊢c>aa]" in exI)
          apply(rule conjI)
           apply(rule crename_interesting1)
           apply(simp)
          apply(rule l_redu.intros)
            apply(simp)
           apply(simp add: fresh_atm)
          apply(auto dest: fic_crename simp add: fresh_prod fresh_atm)[1]
         apply(simp add: trm.inject)
         apply(rule_tac x="M'[a⊢c>b]" in exI)
         apply(rule conjI)
          apply(rule crename_interesting2)
              apply(simp)
             apply(simp)
            apply(simp)
           apply(simp)
          apply(simp)
         apply(rule l_redu.intros)
           apply(simp)
          apply(simp add: fresh_atm)
         apply(auto dest: fic_crename simp add: fresh_prod fresh_atm)[1]
        apply(drule sym)
        apply(drule crename_Cut)
          apply(simp add: fresh_prod fresh_atm)
         apply(simp add: fresh_prod fresh_atm)
        apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
        apply(case_tac "aa=b")
         apply(simp add: crename_id)
         apply(rule l_redu.intros)
           apply(simp)
          apply(simp add: fresh_atm)
         apply(assumption)
        apply(frule crename_ax2)
        apply(auto)[1]
        apply(case_tac "d=aa")
         apply(simp add: trm.inject)
        apply(simp add: trm.inject)
        apply(rule_tac x="N'[x⊢n>y]" in exI)
        apply(rule conjI)
         apply(rule sym)
         apply(rule crename_interesting3)
        apply(rule l_redu.intros)
          apply(simp)
         apply(simp add: fresh_atm)
        apply(auto dest: fin_crename simp add: fresh_prod fresh_atm)[1]
    (* LNot *)
       apply(drule sym)
       apply(drule crename_Cut)
         apply(simp add: fresh_prod abs_fresh fresh_atm)
        apply(simp add: fresh_prod abs_fresh fresh_atm)
       apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
       apply(drule crename_NotR)
         apply(simp add: fresh_prod abs_fresh fresh_atm)
        apply(simp add: fresh_prod abs_fresh fresh_atm)
       apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
       apply(drule crename_NotL)
        apply(simp add: fresh_prod abs_fresh fresh_atm)
       apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
       apply(rule_tac x="Cut <b>.N'b (x).N'a" in exI)
       apply(simp add: fresh_atm)[1]
       apply(rule l_redu.intros)
            apply(auto simp add: fresh_prod intro: crename_fresh_interesting2)[1]
           apply(auto simp add: fresh_atm fresh_prod intro: crename_fresh_interesting2)[1]
          apply(auto simp add: fresh_atm fresh_prod intro: crename_fresh_interesting1)[1]
         apply(auto simp add: fresh_atm fresh_prod intro: crename_fresh_interesting1)[1]
        apply(simp add: fresh_atm)
       apply(simp add: fresh_atm)
    (* LAnd1 *)
      apply(auto dest: fin_crename simp add: fresh_prod fresh_atm)[1]
      apply(drule sym)
      apply(drule crename_Cut)
        apply(simp add: fresh_prod abs_fresh fresh_atm)
       apply(simp add: fresh_prod abs_fresh fresh_atm)
      apply(auto)[1]
      apply(drule crename_AndR)
         apply(simp add: fresh_prod abs_fresh fresh_atm)
        apply(simp add: fresh_prod abs_fresh fresh_atm)
       apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
      apply(drule crename_AndL1)
       apply(simp add: fresh_prod abs_fresh fresh_atm)
      apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
      apply(rule_tac x="Cut <a1>.M'a (x).N'a" in exI)
      apply(simp add: fresh_atm)[1]
      apply(rule l_redu.intros)
           apply(auto simp add: fresh_atm abs_fresh fresh_prod intro: crename_fresh_interesting1)[1]
          apply(auto simp add: abs_fresh fresh_atm fresh_prod intro: crename_fresh_interesting2)[1]
         apply(auto simp add: fresh_atm fresh_prod intro: crename_fresh_interesting1)[1]
        apply(auto simp add: fresh_atm fresh_prod intro: crename_fresh_interesting1)[1]
       apply(simp add: fresh_atm)
      apply(simp add: fresh_atm)
    (* LAnd2 *)
     apply(auto dest: fin_crename simp add: fresh_prod fresh_atm)[1]
     apply(drule sym)
     apply(drule crename_Cut)
       apply(simp add: fresh_prod abs_fresh fresh_atm)
      apply(simp add: fresh_prod abs_fresh fresh_atm)
     apply(auto)[1]
     apply(drule crename_AndR)
        apply(simp add: fresh_prod abs_fresh fresh_atm)
       apply(simp add: fresh_prod abs_fresh fresh_atm)
      apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
     apply(drule crename_AndL2)
      apply(simp add: fresh_prod abs_fresh fresh_atm)
     apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
     apply(rule_tac x="Cut <a2>.N'b (x).N'a" in exI)
     apply(simp add: fresh_atm)[1]
     apply(rule l_redu.intros)
          apply(auto simp add: fresh_atm abs_fresh fresh_prod intro: crename_fresh_interesting1)[1]
         apply(auto simp add: abs_fresh fresh_atm fresh_prod intro: crename_fresh_interesting2)[1]
        apply(auto simp add: fresh_atm fresh_prod intro: crename_fresh_interesting1)[1]
       apply(auto simp add: fresh_atm fresh_prod intro: crename_fresh_interesting1)[1]
      apply(simp add: fresh_atm)
     apply(simp add: fresh_atm)
    (* LOr1 *)
    apply(auto dest: fin_crename simp add: fresh_prod fresh_atm)[1]
    apply(drule sym)
    apply(drule crename_Cut)
      apply(simp add: fresh_prod abs_fresh fresh_atm)
     apply(simp add: fresh_prod abs_fresh fresh_atm)
    apply(auto)[1]
    apply(drule crename_OrL)
      apply(simp add: fresh_prod abs_fresh fresh_atm)
     apply(simp add: fresh_prod abs_fresh fresh_atm)
    apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
    apply(drule crename_OrR1)
      apply(simp add: fresh_prod abs_fresh fresh_atm)
     apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
    apply(auto)
    apply(rule_tac x="Cut <a>.N' (x1).M'a" in exI)
    apply(rule conjI)
     apply(simp add: abs_fresh fresh_atm)[1]
    apply(rule l_redu.intros)
         apply(auto simp add: fresh_atm abs_fresh fresh_prod intro: crename_fresh_interesting1)[1]
        apply(auto simp add: abs_fresh fresh_atm fresh_prod intro: crename_fresh_interesting2)[1]
       apply(auto simp add: abs_fresh fresh_atm fresh_prod intro: crename_fresh_interesting1)[1]
      apply(auto simp add: abs_fresh fresh_atm fresh_prod intro: crename_fresh_interesting1)[1]
     apply(simp add: fresh_atm)
    apply(simp add: fresh_atm)
    (* LOr2 *)
   apply(auto dest: fin_crename simp add: fresh_prod fresh_atm)[1]
   apply(drule sym)
   apply(drule crename_Cut)
     apply(simp add: fresh_prod abs_fresh fresh_atm)
    apply(simp add: fresh_prod abs_fresh fresh_atm)
   apply(auto)[1]
   apply(drule crename_OrL)
     apply(simp add: fresh_prod abs_fresh fresh_atm)
    apply(simp add: fresh_prod abs_fresh fresh_atm)
   apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
   apply(drule crename_OrR2)
     apply(simp add: fresh_prod abs_fresh fresh_atm)
    apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
   apply(auto)
   apply(rule_tac x="Cut <a>.N' (x2).N'a" in exI)
   apply(rule conjI)
    apply(simp add: abs_fresh fresh_atm)[1]
   apply(rule l_redu.intros)
        apply(auto simp add: fresh_atm abs_fresh fresh_prod intro: crename_fresh_interesting1)[1]
       apply(auto simp add: abs_fresh fresh_atm fresh_prod intro: crename_fresh_interesting2)[1]
      apply(auto simp add: abs_fresh fresh_atm fresh_prod intro: crename_fresh_interesting1)[1]
     apply(auto simp add: abs_fresh fresh_atm fresh_prod intro: crename_fresh_interesting1)[1]
    apply(simp add: fresh_atm)
   apply(simp add: fresh_atm)
    (* ImpL *)
  apply(auto dest: fin_crename simp add: fresh_prod fresh_atm)[1]
  apply(drule sym)
  apply(drule crename_Cut)
    apply(simp add: fresh_prod abs_fresh fresh_atm)
   apply(simp add: fresh_prod abs_fresh fresh_atm abs_supp fin_supp)
  apply(auto)[1]
  apply(drule crename_ImpL)
    apply(simp add: fresh_prod abs_fresh fresh_atm)
   apply(simp add: fresh_prod abs_fresh fresh_atm)
  apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
  apply(drule crename_ImpR)
     apply(simp add: fresh_prod abs_fresh fresh_atm)
    apply(simp add: fresh_prod abs_fresh fresh_atm)
   apply(simp)
  apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
  apply(rule_tac x="Cut <a>.(Cut <c>.M'a (x).N') (y).N'a" in exI)
  apply(rule conjI)
   apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
  apply(rule l_redu.intros)
       apply(auto simp add: fresh_atm abs_fresh abs_supp fin_supp fresh_prod intro: crename_fresh_interesting2)[1]
      apply(auto simp add: abs_fresh fresh_atm abs_supp fin_supp fresh_prod intro: crename_fresh_interesting1)[1]
     apply(auto simp add: abs_fresh fresh_atm abs_supp fin_supp fresh_prod intro: crename_fresh_interesting2)[1]
    apply(auto simp add: abs_fresh fresh_atm abs_supp fin_supp fresh_prod intro: crename_fresh_interesting1)[1]
   apply(auto simp add: abs_fresh fresh_atm abs_supp fin_supp fresh_prod intro: crename_fresh_interesting1)[1]
  apply(auto simp add: abs_fresh fresh_atm abs_supp fin_supp fresh_prod intro: crename_fresh_interesting1)[1]
  done

lemma crename_aredu:
  assumes a: "(M[a⊢c>b]) ⟶⇩a M'" "a≠b"
  shows "∃M0. M0[a⊢c>b]=M' ∧ M ⟶⇩a M0"
  using a
  apply(nominal_induct "M[a⊢c>b]" M' avoiding: M a b rule: a_redu.strong_induct)
                  apply(drule  crename_lredu)
                  apply(blast)
                 apply(drule  crename_credu)
                 apply(blast)
    (* Cut *)
                apply(drule sym)
                apply(drule crename_Cut)
                  apply(simp)
                 apply(simp)
                apply(auto)[1]
                apply(drule_tac x="M'a" in meta_spec)
                apply(drule_tac x="aa" in meta_spec)
                apply(drule_tac x="b" in meta_spec)
                apply(auto)[1]
                apply(rule_tac x="Cut <a>.M0 (x).N'" in exI)
                apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
                apply(rule conjI)
                 apply(rule trans)
                  apply(rule crename.simps)
                   apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
                  apply(drule crename_fresh_interesting2)
                  apply(simp add: fresh_a_redu)
                 apply(simp)
                apply(auto)[1]
               apply(drule sym)
               apply(drule crename_Cut)
                 apply(simp)
                apply(simp)
               apply(auto)[1]
               apply(drule_tac x="N'a" in meta_spec)
               apply(drule_tac x="aa" in meta_spec)
               apply(drule_tac x="b" in meta_spec)
               apply(auto)[1]
               apply(rule_tac x="Cut <a>.M' (x).M0" in exI)
               apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
               apply(rule conjI)
                apply(rule trans)
                 apply(rule crename.simps)
                  apply(simp add: abs_fresh abs_supp fin_supp fresh_atm fresh_prod)[1]
                  apply(drule crename_fresh_interesting1)
                   apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
                  apply(simp add: fresh_a_redu)
                 apply(simp)
                apply(simp)
               apply(auto)[1]
    (* NotL *)
              apply(drule sym)
              apply(drule crename_NotL)
               apply(simp)
              apply(auto)[1]
              apply(drule_tac x="N'" in meta_spec)
              apply(drule_tac x="aa" in meta_spec)
              apply(drule_tac x="b" in meta_spec)
              apply(auto)[1]
              apply(rule_tac x="NotL <a>.M0 x" in exI)
              apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
              apply(auto)[1]
    (* NotR *)
             apply(drule sym)
             apply(frule crename_NotR_aux)
             apply(erule disjE)
              apply(auto)[1]
             apply(drule crename_NotR')
               apply(simp)
              apply(simp add: fresh_atm)
             apply(erule disjE)
              apply(auto)[1]
              apply(drule_tac x="N'" in meta_spec)
              apply(drule_tac x="aa" in meta_spec)
              apply(drule_tac x="b" in meta_spec)
              apply(auto)[1]
              apply(rule_tac x="NotR (x).M0 a" in exI)
              apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
              apply(auto)[1]
             apply(auto)[1]
             apply(drule_tac x="N'" in meta_spec)
             apply(drule_tac x="aa" in meta_spec)
             apply(drule_tac x="a" in meta_spec)
             apply(auto)[1]
             apply(rule_tac x="NotR (x).M0 aa" in exI)
             apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
             apply(auto)[1]
    (* AndR *)
            apply(drule sym)
            apply(frule crename_AndR_aux)
            apply(erule disjE)
             apply(auto)[1]
            apply(drule crename_AndR')
               apply(simp add: fresh_prod fresh_atm)
              apply(simp add: fresh_atm)
             apply(simp add: fresh_atm)
            apply(erule disjE)
             apply(auto)[1]
             apply(drule_tac x="M'a" in meta_spec)
             apply(drule_tac x="aa" in meta_spec)
             apply(drule_tac x="ba" in meta_spec)
             apply(auto)[1]
             apply(rule_tac x="AndR <a>.M0 <b>.N' c" in exI)
             apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
             apply(auto)[1]
             apply(rule trans)
              apply(rule crename.simps)
                apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
               apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
               apply(auto intro: fresh_a_redu)[1]
              apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
             apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
            apply(auto)[1]
            apply(drule_tac x="M'a" in meta_spec)
            apply(drule_tac x="aa" in meta_spec)
            apply(drule_tac x="c" in meta_spec)
            apply(auto)[1]
            apply(rule_tac x="AndR <a>.M0 <b>.N' aa" in exI)
            apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
            apply(auto)[1]
            apply(rule trans)
             apply(rule crename.simps)
               apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
              apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
              apply(auto intro: fresh_a_redu)[1]
             apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
            apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
           apply(drule sym)
           apply(frule crename_AndR_aux)
           apply(erule disjE)
            apply(auto)[1]
           apply(drule crename_AndR')
              apply(simp add: fresh_prod fresh_atm)
             apply(simp add: fresh_atm)
            apply(simp add: fresh_atm)
           apply(erule disjE)
            apply(auto)[1]
            apply(drule_tac x="N'a" in meta_spec)
            apply(drule_tac x="aa" in meta_spec)
            apply(drule_tac x="ba" in meta_spec)
            apply(auto)[1]
            apply(rule_tac x="AndR <a>.M' <b>.M0 c" in exI)
            apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
            apply(auto)[1]
            apply(rule trans)
             apply(rule crename.simps)
               apply(simp add: abs_fresh abs_supp fin_supp fresh_atm fresh_prod)[1]
               apply(auto intro: fresh_a_redu)[1]
              apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
             apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
            apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
           apply(auto)[1]
           apply(drule_tac x="N'a" in meta_spec)
           apply(drule_tac x="aa" in meta_spec)
           apply(drule_tac x="c" in meta_spec)
           apply(auto)[1]
           apply(rule_tac x="AndR <a>.M' <b>.M0 aa" in exI)
           apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
           apply(auto)[1]
           apply(rule trans)
            apply(rule crename.simps)
              apply(simp add: abs_fresh abs_supp fin_supp fresh_atm fresh_prod)[1]
              apply(auto intro: fresh_a_redu)[1]
             apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
            apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
           apply(simp)
    (* AndL1 *)
          apply(drule sym)
          apply(drule crename_AndL1)
           apply(simp)
          apply(auto)[1]
          apply(drule_tac x="N'" in meta_spec)
          apply(drule_tac x="a" in meta_spec)
          apply(drule_tac x="b" in meta_spec)
          apply(auto)[1]
          apply(rule_tac x="AndL1 (x).M0 y" in exI)
          apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
          apply(auto)[1]
    (* AndL2 *)
         apply(drule sym)
         apply(drule crename_AndL2)
          apply(simp)
         apply(auto)[1]
         apply(drule_tac x="N'" in meta_spec)
         apply(drule_tac x="a" in meta_spec)
         apply(drule_tac x="b" in meta_spec)
         apply(auto)[1]
         apply(rule_tac x="AndL2 (x).M0 y" in exI)
         apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
         apply(auto)[1]
    (* OrL *)
        apply(drule sym)
        apply(drule crename_OrL)
          apply(simp)
          apply(auto simp add: fresh_atm fresh_prod)[1]
         apply(auto simp add: fresh_atm fresh_prod)[1]
        apply(auto)[1]
        apply(drule_tac x="M'a" in meta_spec)
        apply(drule_tac x="a" in meta_spec)
        apply(drule_tac x="b" in meta_spec)
        apply(auto)[1]
        apply(rule_tac x="OrL (x).M0 (y).N' z" in exI)
        apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
        apply(auto)[1]
        apply(rule trans)
         apply(rule crename.simps)
           apply(simp add: abs_fresh abs_supp fin_supp fresh_atm fresh_prod)[1]
          apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
          apply(auto intro: fresh_a_redu)[1]
         apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
        apply(simp)
       apply(drule sym)
       apply(drule crename_OrL)
         apply(simp)
         apply(auto simp add: fresh_atm fresh_prod)[1]
        apply(auto simp add: fresh_atm fresh_prod)[1]
       apply(auto)[1]
       apply(drule_tac x="N'a" in meta_spec)
       apply(drule_tac x="a" in meta_spec)
       apply(drule_tac x="b" in meta_spec)
       apply(auto)[1]
       apply(rule_tac x="OrL (x).M' (y).M0 z" in exI)
       apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
       apply(auto)[1]
       apply(rule trans)
        apply(rule crename.simps)
          apply(simp add: abs_fresh abs_supp fin_supp fresh_atm fresh_prod)[1]
          apply(auto intro: fresh_a_redu)[1]
         apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
        apply(simp)
       apply(simp)
    (* OrR1 *)
      apply(drule sym)
      apply(frule crename_OrR1_aux)
      apply(erule disjE)
       apply(auto)[1]
      apply(drule crename_OrR1')
        apply(simp)
       apply(simp add: fresh_atm)
      apply(erule disjE)
       apply(auto)[1]
       apply(drule_tac x="N'" in meta_spec)
       apply(drule_tac x="aa" in meta_spec)
       apply(drule_tac x="ba" in meta_spec)
       apply(auto)[1]
       apply(rule_tac x="OrR1 <a>.M0 b" in exI)
       apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
       apply(auto)[1]
      apply(auto)[1]
      apply(drule_tac x="N'" in meta_spec)
      apply(drule_tac x="aa" in meta_spec)
      apply(drule_tac x="b" in meta_spec)
      apply(auto)[1]
      apply(rule_tac x="OrR1 <a>.M0 aa" in exI)
      apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
      apply(auto)[1]
    (* OrR2 *)
     apply(drule sym)
     apply(frule crename_OrR2_aux)
     apply(erule disjE)
      apply(auto)[1]
     apply(drule crename_OrR2')
       apply(simp)
      apply(simp add: fresh_atm)
     apply(erule disjE)
      apply(auto)[1]
      apply(drule_tac x="N'" in meta_spec)
      apply(drule_tac x="aa" in meta_spec)
      apply(drule_tac x="ba" in meta_spec)
      apply(auto)[1]
      apply(rule_tac x="OrR2 <a>.M0 b" in exI)
      apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
      apply(auto)[1]
     apply(auto)[1]
     apply(drule_tac x="N'" in meta_spec)
     apply(drule_tac x="aa" in meta_spec)
     apply(drule_tac x="b" in meta_spec)
     apply(auto)[1]
     apply(rule_tac x="OrR2 <a>.M0 aa" in exI)
     apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
     apply(auto)[1]
    (* ImpL *)
    apply(drule sym)
    apply(drule crename_ImpL)
      apply(simp)
     apply(simp)
    apply(auto)[1]
    apply(drule_tac x="M'a" in meta_spec)
    apply(drule_tac x="aa" in meta_spec)
    apply(drule_tac x="b" in meta_spec)
    apply(auto)[1]
    apply(rule_tac x="ImpL <a>.M0 (x).N' y" in exI)
    apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
    apply(auto)[1]
    apply(rule trans)
     apply(rule crename.simps)
      apply(simp add: abs_fresh abs_supp fin_supp fresh_atm fresh_prod)[1]
     apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
     apply(auto intro: fresh_a_redu)[1]
    apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
   apply(drule sym)
   apply(drule crename_ImpL)
     apply(simp)
    apply(simp)
   apply(auto)[1]
   apply(drule_tac x="N'a" in meta_spec)
   apply(drule_tac x="aa" in meta_spec)
   apply(drule_tac x="b" in meta_spec)
   apply(auto)[1]
   apply(rule_tac x="ImpL <a>.M' (x).M0 y" in exI)
   apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
   apply(auto)[1]
   apply(rule trans)
    apply(rule crename.simps)
     apply(simp add: abs_fresh abs_supp fin_supp fresh_atm fresh_prod)[1]
     apply(auto intro: fresh_a_redu)[1]
    apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
   apply(simp)
    (* ImpR *)
  apply(drule sym)
  apply(frule crename_ImpR_aux)
  apply(erule disjE)
   apply(auto)[1]
  apply(drule crename_ImpR')
     apply(simp)
    apply(simp add: fresh_atm)
   apply(simp add: fresh_atm)
  apply(erule disjE)
   apply(auto)[1]
   apply(drule_tac x="N'" in meta_spec)
   apply(drule_tac x="aa" in meta_spec)
   apply(drule_tac x="ba" in meta_spec)
   apply(auto)[1]
   apply(rule_tac x="ImpR (x).<a>.M0 b" in exI)
   apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
   apply(auto)[1]
  apply(auto)[1]
  apply(drule_tac x="N'" in meta_spec)
  apply(drule_tac x="aa" in meta_spec)
  apply(drule_tac x="b" in meta_spec)
  apply(auto)[1]
  apply(rule_tac x="ImpR (x).<a>.M0 aa" in exI)
  apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
  apply(auto)[1]
  done

lemma SNa_preserved_renaming1:
  assumes a: "SNa M"
  shows "SNa (M[a⊢c>b])"
  using a
  apply(induct rule: SNa_induct)
  apply(case_tac "a=b")
   apply(simp add: crename_id)
  apply(rule SNaI)
  apply(drule crename_aredu)
   apply(blast)+
  done

lemma nrename_interesting1:
  assumes a: "distinct [x,y,z]"
  shows "M[x⊢n>z][z⊢n>y] = M[z⊢n>y][x⊢n>y]"
  using a
  apply(nominal_induct M avoiding: x y z rule: trm.strong_induct)
             apply(auto simp add: rename_fresh simp add: trm.inject alpha)
     apply(blast)
    apply(blast)
   apply(rotate_tac 12)
   apply(drule_tac x="x" in meta_spec)
   apply(rotate_tac 15)
   apply(drule_tac x="y" in meta_spec)
   apply(rotate_tac 15)
   apply(drule_tac x="z" in meta_spec)
   apply(blast)
  apply(rotate_tac 11)
  apply(drule_tac x="x" in meta_spec)
  apply(rotate_tac 14)
  apply(drule_tac x="y" in meta_spec)
  apply(rotate_tac 14)
  apply(drule_tac x="z" in meta_spec)
  apply(blast)
  done

lemma nrename_interesting2:
  assumes a: "x≠z" "x≠u" "x≠y" "z≠u" "y≠z"
  shows "M[x⊢n>y][z⊢n>u] = M[z⊢n>u][x⊢n>y]"
  using a
  apply(nominal_induct M avoiding: x y z u rule: trm.strong_induct)
             apply(auto simp add: rename_fresh simp add: trm.inject alpha)
  done

lemma not_fic_nrename_aux:
  assumes a: "fic M c" 
  shows "fic (M[x⊢n>y]) c" 
  using a
  apply(nominal_induct M avoiding: c x y rule: trm.strong_induct)
             apply(auto dest!: fic_elims intro!: fic.intros simp add: fresh_prod fresh_atm rename_fresh abs_fresh)
  done

lemma not_fic_nrename:
  assumes a: "¬(fic (M[x⊢n>y]) c)" 
  shows "¬(fic M c)" 
  using a
  apply(auto dest:  not_fic_nrename_aux)
  done

lemma fin_nrename:
  assumes a: "fin M z" "z♯(x,y)"
  shows "fin (M[x⊢n>y]) z" 
  using a
  apply(nominal_induct M avoiding: x y z rule: trm.strong_induct)
             apply(auto dest!: fin_elims intro!: fin.intros simp add: fresh_prod fresh_atm rename_fresh abs_fresh
      split: if_splits)
  done

lemma nrename_fresh_interesting1:
  fixes z::"name"
  assumes a: "z♯(M[x⊢n>y])" "z♯(x,y)"
  shows "z♯M"
  using a
  apply(nominal_induct M avoiding: x y z rule: trm.strong_induct)
             apply(auto split: if_splits simp add: abs_fresh abs_supp fin_supp)
  done

lemma nrename_fresh_interesting2:
  fixes c::"coname"
  assumes a: "c♯(M[x⊢n>y])" 
  shows "c♯M"
  using a
  apply(nominal_induct M avoiding: x y c rule: trm.strong_induct)
             apply(auto split: if_splits simp add: abs_fresh abs_supp fin_supp fresh_atm)
  done

lemma fin_nrename2:
  assumes a: "fin (M[x⊢n>y]) z" "z♯(x,y)"
  shows "fin M z" 
  using a
  apply(nominal_induct M avoiding: x y z rule: trm.strong_induct)
             apply(auto dest!: fin_elims intro!: fin.intros simp add: fresh_prod fresh_atm rename_fresh abs_fresh
      split: if_splits)
        apply(auto dest: nrename_fresh_interesting1 simp add: fresh_atm fresh_prod)
  done

lemma nrename_Cut:
  assumes a: "R[x⊢n>y] = Cut <c>.M (z).N" "c♯(N,R)" "z♯(x,y,M,R)"
  shows "∃M' N'. R = Cut <c>.M' (z).N' ∧ M'[x⊢n>y] = M ∧ N'[x⊢n>y] = N ∧ c♯N' ∧ z♯M'"
  using a
  apply(nominal_induct R avoiding: c y x z M N rule: trm.strong_induct)
             apply(auto split: if_splits)
  apply(simp add: trm.inject)
  apply(auto simp add: alpha fresh_atm)
  apply(rule_tac x="[(coname,c)]∙trm1" in exI)
  apply(perm_simp)
  apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
  apply(rule_tac x="[(name,z)]∙trm2" in exI)
  apply(perm_simp)
  apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
  apply(rule conjI)
   apply(drule sym)
   apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
   apply(simp add: eqvts calc_atm)
  apply(auto simp add: fresh_atm)[1]
  apply(drule sym)
  apply(drule sym)
  apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
  apply(simp add: eqvts calc_atm)
  done

lemma nrename_NotR:
  assumes a: "R[x⊢n>y] = NotR (z).N c" "z♯(R,x,y)" 
  shows "∃N'. (R = NotR (z).N' c) ∧ N'[x⊢n>y] = N" 
  using a
  apply(nominal_induct R avoiding: x y c z N rule: trm.strong_induct)
             apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
  apply(rule_tac x="[(name,z)]∙trm" in exI)
  apply(perm_simp)
  apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
  apply(drule sym)
  apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
  apply(simp add: eqvts calc_atm)
  done

lemma nrename_NotL:
  assumes a: "R[x⊢n>y] = NotL <c>.N z" "c♯R" "z♯(x,y)"
  shows "∃N'. (R = NotL <c>.N' z) ∧ N'[x⊢n>y] = N" 
  using a
  apply(nominal_induct R avoiding: x y c z N rule: trm.strong_induct)
             apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
  apply(rule_tac x="[(coname,c)]∙trm" in exI)
  apply(perm_simp)
  apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
  apply(drule sym)
  apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
  apply(simp add: eqvts calc_atm)
  done

lemma nrename_NotL':
  assumes a: "R[x⊢n>y] = NotL <c>.N u" "c♯R" "x≠y" 
  shows "(∃N'. (R = NotL <c>.N' u) ∧ N'[x⊢n>y] = N) ∨ (∃N'. (R = NotL <c>.N' x) ∧ y=u ∧ N'[x⊢n>y] = N)"
  using a
  apply(nominal_induct R avoiding: y u c x N rule: trm.strong_induct)
             apply(auto split: if_splits simp add: fresh_prod fresh_atm abs_fresh alpha trm.inject)
   apply(rule_tac x="[(coname,c)]∙trm" in exI)
   apply(perm_simp)
   apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
   apply(drule sym)
   apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
   apply(simp add: eqvts calc_atm)
  apply(rule_tac x="[(coname,c)]∙trm" in exI)
  apply(perm_simp)
  apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
  apply(drule sym)
  apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
  apply(simp add: eqvts calc_atm)
  done

lemma nrename_NotL_aux:
  assumes a: "R[x⊢n>y] = NotL <c>.N u" 
  shows "(x=u ∧ x=y) ∨ (x≠u)" 
  using a
  apply(nominal_induct R avoiding: y u c x N rule: trm.strong_induct)
             apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
  done

lemma nrename_AndL1:
  assumes a: "R[x⊢n>y] = AndL1 (z).N u" "z♯(R,x,y)" "u♯(x,y)"
  shows "∃N'. (R = AndL1 (z).N' u) ∧ N'[x⊢n>y] = N" 
  using a
  apply(nominal_induct R avoiding: z u x y N rule: trm.strong_induct)
             apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
  apply(rule_tac x="[(name1,z)]∙trm" in exI)
  apply(perm_simp)
  apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
  apply(drule sym)
  apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
  apply(simp add: eqvts calc_atm)
  done

lemma nrename_AndL1':
  assumes a: "R[x⊢n>y] = AndL1 (v).N u" "v♯(R,u,x,y)" "x≠y" 
  shows "(∃N'. (R = AndL1 (v).N' u) ∧ N'[x⊢n>y] = N) ∨ (∃N'. (R = AndL1 (v).N' x) ∧ y=u ∧ N'[x⊢n>y] = N)"
  using a
  apply(nominal_induct R avoiding: y u v x N rule: trm.strong_induct)
             apply(auto split: if_splits simp add: fresh_prod fresh_atm abs_fresh alpha trm.inject)
   apply(rule_tac x="[(name1,v)]∙trm" in exI)
   apply(perm_simp)
   apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
   apply(drule sym)
   apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
   apply(simp add: eqvts calc_atm)
  apply(rule_tac x="[(name1,v)]∙trm" in exI)
  apply(perm_simp)
  apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
  apply(drule sym)
  apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
  apply(simp add: eqvts calc_atm)
  done

lemma nrename_AndL1_aux:
  assumes a: "R[x⊢n>y] = AndL1 (v).N u" 
  shows "(x=u ∧ x=y) ∨ (x≠u)" 
  using a
  apply(nominal_induct R avoiding: y u v x N rule: trm.strong_induct)
             apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
  done

lemma nrename_AndL2:
  assumes a: "R[x⊢n>y] = AndL2 (z).N u" "z♯(R,x,y)" "u♯(x,y)"
  shows "∃N'. (R = AndL2 (z).N' u) ∧ N'[x⊢n>y] = N" 
  using a
  apply(nominal_induct R avoiding: z u x y N rule: trm.strong_induct)
             apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
  apply(rule_tac x="[(name1,z)]∙trm" in exI)
  apply(perm_simp)
  apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
  apply(drule sym)
  apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
  apply(simp add: eqvts calc_atm)
  done

lemma nrename_AndL2':
  assumes a: "R[x⊢n>y] = AndL2 (v).N u" "v♯(R,u,x,y)" "x≠y" 
  shows "(∃N'. (R = AndL2 (v).N' u) ∧ N'[x⊢n>y] = N) ∨ (∃N'. (R = AndL2 (v).N' x) ∧ y=u ∧ N'[x⊢n>y] = N)"
  using a
  apply(nominal_induct R avoiding: y u v x N rule: trm.strong_induct)
             apply(auto split: if_splits simp add: fresh_prod fresh_atm abs_fresh alpha trm.inject)
   apply(rule_tac x="[(name1,v)]∙trm" in exI)
   apply(perm_simp)
   apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
   apply(drule sym)
   apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
   apply(simp add: eqvts calc_atm)
  apply(rule_tac x="[(name1,v)]∙trm" in exI)
  apply(perm_simp)
  apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
  apply(drule sym)
  apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
  apply(simp add: eqvts calc_atm)
  done

lemma nrename_AndL2_aux:
  assumes a: "R[x⊢n>y] = AndL2 (v).N u" 
  shows "(x=u ∧ x=y) ∨ (x≠u)" 
  using a
  apply(nominal_induct R avoiding: y u v x N rule: trm.strong_induct)
             apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
  done

lemma nrename_AndR:
  assumes a: "R[x⊢n>y] = AndR <c>.M <d>.N e" "c♯(d,e,N,R)" "d♯(c,e,M,R)" 
  shows "∃M' N'. R = AndR <c>.M' <d>.N' e ∧ M'[x⊢n>y] = M ∧ N'[x⊢n>y] = N ∧ c♯N' ∧ d♯M'"
  using a
  apply(nominal_induct R avoiding: x y c d e M N rule: trm.strong_induct)
             apply(auto split: if_splits simp add: trm.inject alpha)
    apply(simp add: fresh_atm fresh_prod)
   apply(rule_tac x="[(coname1,c)]∙trm1" in exI)
   apply(perm_simp)
   apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
  apply(rule_tac x="[(coname1,c)]∙trm1" in exI)
  apply(perm_simp)
  apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
  apply(rule_tac x="[(coname2,d)]∙trm2" in exI)
  apply(perm_simp)
  apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
   apply(drule sym)
   apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
   apply(simp add: eqvts calc_atm)
  apply(drule_tac s="trm2[x⊢n>y]" in  sym)
  apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
  apply(simp add: eqvts calc_atm)
  done

lemma nrename_OrR1:
  assumes a: "R[x⊢n>y] = OrR1 <c>.N d" "c♯(R,d)" 
  shows "∃N'. (R = OrR1 <c>.N' d) ∧ N'[x⊢n>y] = N" 
  using a
  apply(nominal_induct R avoiding: x y c d N rule: trm.strong_induct)
             apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
  apply(rule_tac x="[(coname1,c)]∙trm" in exI)
  apply(perm_simp)
  apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
  apply(drule sym)
  apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
  apply(simp add: eqvts calc_atm)
  done

lemma nrename_OrR2:
  assumes a: "R[x⊢n>y] = OrR2 <c>.N d" "c♯(R,d)" 
  shows "∃N'. (R = OrR2 <c>.N' d) ∧ N'[x⊢n>y] = N" 
  using a
  apply(nominal_induct R avoiding: x y c d N rule: trm.strong_induct)
             apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
  apply(rule_tac x="[(coname1,c)]∙trm" in exI)
  apply(perm_simp)
  apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
  apply(drule sym)
  apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
  apply(simp add: eqvts calc_atm)
  done

lemma nrename_OrL:
  assumes a: "R[u⊢n>v] = OrL (x).M (y).N z" "x♯(y,z,u,v,N,R)" "y♯(x,z,u,v,M,R)" "z♯(u,v)"
  shows "∃M' N'. R = OrL (x).M' (y).N' z ∧ M'[u⊢n>v] = M ∧ N'[u⊢n>v] = N ∧ x♯N' ∧ y♯M'"
  using a
  apply(nominal_induct R avoiding: u v x y z M N rule: trm.strong_induct)
             apply(auto split: if_splits simp add: trm.inject alpha fresh_prod fresh_atm)
  apply(rule_tac x="[(name1,x)]∙trm1" in exI)
  apply(perm_simp)
  apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
  apply(rule_tac x="[(name2,y)]∙trm2" in exI)
  apply(perm_simp)
  apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
   apply(drule sym)
   apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
   apply(simp add: eqvts calc_atm)
  apply(drule_tac s="trm2[u⊢n>v]" in  sym)
  apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
  apply(simp add: eqvts calc_atm)
  done

lemma nrename_OrL':
  assumes a: "R[x⊢n>y] = OrL (v).M (w).N u" "v♯(R,N,u,x,y)" "w♯(R,M,u,x,y)" "x≠y" 
  shows "(∃M' N'. (R = OrL (v).M' (w).N' u) ∧ M'[x⊢n>y] = M ∧ N'[x⊢n>y] = N) ∨ 
         (∃M' N'. (R = OrL (v).M' (w).N' x) ∧ y=u ∧ M'[x⊢n>y] = M ∧ N'[x⊢n>y] = N)"
  using a [[simproc del: defined_all]]
  apply(nominal_induct R avoiding: y x u v w M N rule: trm.strong_induct)
             apply(auto split: if_splits simp add: fresh_prod fresh_atm abs_fresh alpha trm.inject)
   apply(rule_tac x="[(name1,v)]∙trm1" in exI)
   apply(perm_simp)
   apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
   apply(rule_tac x="[(name2,w)]∙trm2" in exI)
   apply(perm_simp)
   apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
   apply(rule conjI)
    apply(drule sym)
    apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
    apply(simp add: eqvts calc_atm)
   apply(drule_tac s="trm2[x⊢n>u]" in sym)
   apply(drule_tac pt_bij1[OF pt_name_inst,OF at_name_inst])
   apply(simp add: eqvts calc_atm)
  apply(rule_tac x="[(name1,v)]∙trm1" in exI)
  apply(perm_simp)
  apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
  apply(rule_tac x="[(name2,w)]∙trm2" in exI)
  apply(perm_simp)
  apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
  apply(rule conjI)
   apply(drule sym)
   apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
   apply(simp add: eqvts calc_atm)
  apply(drule_tac s="trm2[x⊢n>y]" in sym)
  apply(drule_tac pt_bij1[OF pt_name_inst,OF at_name_inst])
  apply(simp add: eqvts calc_atm)
  done

lemma nrename_OrL_aux:
  assumes a: "R[x⊢n>y] = OrL (v).M (w).N u" 
  shows "(x=u ∧ x=y) ∨ (x≠u)" 
  using a
  apply(nominal_induct R avoiding: y x w u v M N rule: trm.strong_induct)
             apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
  done

lemma nrename_ImpL:
  assumes a: "R[x⊢n>y] = ImpL <c>.M (u).N z" "c♯(N,R)" "u♯(y,x,z,M,R)" "z♯(x,y)"
  shows "∃M' N'. R = ImpL <c>.M' (u).N' z ∧ M'[x⊢n>y] = M ∧ N'[x⊢n>y] = N ∧ c♯N' ∧ u♯M'"
  using a
  apply(nominal_induct R avoiding: u x c y z M N rule: trm.strong_induct)
             apply(auto split: if_splits simp add: trm.inject alpha fresh_prod fresh_atm)
  apply(rule_tac x="[(coname,c)]∙trm1" in exI)
  apply(perm_simp)
  apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
  apply(rule_tac x="[(name1,u)]∙trm2" in exI)
  apply(perm_simp)
  apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
   apply(drule sym)
   apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
   apply(simp add: eqvts calc_atm)
  apply(drule_tac s="trm2[x⊢n>y]" in  sym)
  apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
  apply(simp add: eqvts calc_atm fresh_prod fresh_atm)
  done

lemma nrename_ImpL':
  assumes a: "R[x⊢n>y] = ImpL <c>.M (w).N u" "c♯(R,N)" "w♯(R,M,u,x,y)" "x≠y" 
  shows "(∃M' N'. (R = ImpL <c>.M' (w).N' u) ∧ M'[x⊢n>y] = M ∧ N'[x⊢n>y] = N) ∨ 
         (∃M' N'. (R = ImpL <c>.M' (w).N' x) ∧ y=u ∧ M'[x⊢n>y] = M ∧ N'[x⊢n>y] = N)"
  using a [[simproc del: defined_all]]
  apply(nominal_induct R avoiding: y x u c w M N rule: trm.strong_induct)
             apply(auto split: if_splits simp add: fresh_prod fresh_atm abs_fresh alpha trm.inject)
   apply(rule_tac x="[(coname,c)]∙trm1" in exI)
   apply(perm_simp)
   apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
   apply(rule_tac x="[(name1,w)]∙trm2" in exI)
   apply(perm_simp)
   apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
   apply(rule conjI)
    apply(drule sym)
    apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
    apply(simp add: eqvts calc_atm)
   apply(drule_tac s="trm2[x⊢n>u]" in sym)
   apply(drule_tac pt_bij1[OF pt_name_inst,OF at_name_inst])
   apply(simp add: eqvts calc_atm)
  apply(rule_tac x="[(coname,c)]∙trm1" in exI)
  apply(perm_simp)
  apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
  apply(rule_tac x="[(name1,w)]∙trm2" in exI)
  apply(perm_simp)
  apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
  apply(rule conjI)
   apply(drule sym)
   apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
   apply(simp add: eqvts calc_atm)
  apply(drule_tac s="trm2[x⊢n>y]" in sym)
  apply(drule_tac pt_bij1[OF pt_name_inst,OF at_name_inst])
  apply(simp add: eqvts calc_atm)
  done

lemma nrename_ImpL_aux:
  assumes a: "R[x⊢n>y] = ImpL <c>.M (w).N u" 
  shows "(x=u ∧ x=y) ∨ (x≠u)" 
  using a
  apply(nominal_induct R avoiding: y x w u c M N rule: trm.strong_induct)
             apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
  done

lemma nrename_ImpR:
  assumes a: "R[u⊢n>v] = ImpR (x).<c>.N d" "c♯(R,d)" "x♯(R,u,v)" 
  shows "∃N'. (R = ImpR (x).<c>.N' d) ∧ N'[u⊢n>v] = N" 
  using a
  apply(nominal_induct R avoiding: u v x c d N rule: trm.strong_induct)
             apply(auto split: if_splits simp add: fresh_prod fresh_atm abs_perm alpha abs_fresh trm.inject)
   apply(rule_tac x="[(name,x)]∙trm" in exI)
   apply(perm_simp)
  apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
  apply(rule_tac x="[(name,x)]∙[(coname1, c)]∙trm" in exI)
  apply(perm_simp)
  apply(simp add: abs_supp fin_supp abs_fresh fresh_left calc_atm fresh_prod)
  apply(drule sym)
  apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
  apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
  apply(simp add: eqvts calc_atm)
  done

lemma nrename_credu:
  assumes a: "(M[x⊢n>y]) ⟶⇩c M'"
  shows "∃M0. M0[x⊢n>y]=M' ∧ M ⟶⇩c M0"
  using a
  apply(nominal_induct M≡"M[x⊢n>y]" M' avoiding: M x y rule: c_redu.strong_induct)
   apply(drule sym)
   apply(drule nrename_Cut)
     apply(simp)
    apply(simp)
   apply(auto)
   apply(rule_tac x="M'{a:=(x).N'}" in exI)
   apply(rule conjI)
    apply(simp add: fresh_atm abs_fresh subst_comm fresh_prod)
   apply(rule c_redu.intros)
     apply(auto dest: not_fic_nrename)[1]
    apply(simp add: abs_fresh)
   apply(simp add: abs_fresh)
  apply(drule sym)
  apply(drule nrename_Cut)
    apply(simp)
   apply(simp)
  apply(auto)
  apply(rule_tac x="N'{x:=<a>.M'}" in exI)
  apply(rule conjI)
   apply(simp add: fresh_atm abs_fresh subst_comm fresh_prod)
  apply(rule c_redu.intros)
    apply(auto)
  apply(drule_tac x="xa" and y="y" in fin_nrename)
   apply(auto simp add: fresh_prod abs_fresh)
  done

lemma nrename_ax2:
  assumes a: "N[x⊢n>y] = Ax z c"
  shows "∃z. N = Ax z c"
  using a
  apply(nominal_induct N avoiding: x y rule: trm.strong_induct)
             apply(auto split: if_splits)
  apply(simp add: trm.inject)
  done

lemma fic_nrename:
  assumes a: "fic (M[x⊢n>y]) c" 
  shows "fic M c" 
  using a
  apply(nominal_induct M avoiding: c x y rule: trm.strong_induct)
             apply(auto dest!: fic_elims intro!: fic.intros simp add: fresh_prod fresh_atm rename_fresh abs_fresh
      split: if_splits)
       apply(auto dest: nrename_fresh_interesting2 simp add: fresh_prod fresh_atm)
  done

lemma nrename_lredu:
  assumes a: "(M[x⊢n>y]) ⟶⇩l M'"
  shows "∃M0. M0[x⊢n>y]=M' ∧ M ⟶⇩l M0"
  using a
  apply(nominal_induct M≡"M[x⊢n>y]" M' avoiding: M x y rule: l_redu.strong_induct)
         apply(drule sym)
         apply(drule nrename_Cut)
           apply(simp add: fresh_prod fresh_atm)
          apply(simp)
         apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
         apply(case_tac "xa=y")
          apply(simp add: nrename_id)
          apply(rule l_redu.intros)
            apply(simp)
           apply(simp add: fresh_atm)
          apply(assumption)
         apply(frule nrename_ax2)
         apply(auto)[1]
         apply(case_tac "z=xa")
          apply(simp add: trm.inject)
         apply(simp)
         apply(rule_tac x="M'[a⊢c>b]" in exI)
         apply(rule conjI)
          apply(rule crename_interesting3)
         apply(rule l_redu.intros)
           apply(simp)
          apply(simp add: fresh_atm)
         apply(auto dest: fic_nrename simp add: fresh_prod fresh_atm)[1]
        apply(drule sym)
        apply(drule nrename_Cut)
          apply(simp add: fresh_prod fresh_atm)
         apply(simp add: fresh_prod fresh_atm)
        apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
        apply(case_tac "xa=ya")
         apply(simp add: nrename_id)
         apply(rule l_redu.intros)
           apply(simp)
          apply(simp add: fresh_atm)
         apply(assumption)
        apply(frule nrename_ax2)
        apply(auto)[1]
        apply(case_tac "z=xa")
         apply(simp add: trm.inject)
         apply(rule_tac x="N'[x⊢n>xa]" in exI)
         apply(rule conjI)
          apply(rule nrename_interesting1)
          apply(auto)[1]
         apply(rule l_redu.intros)
           apply(simp)
          apply(simp add: fresh_atm)
         apply(auto dest: fin_nrename2 simp add: fresh_prod fresh_atm)[1]
        apply(simp add: trm.inject)
        apply(rule_tac x="N'[x⊢n>y]" in exI)
        apply(rule conjI)
         apply(rule nrename_interesting2)
             apply(simp_all)
        apply(rule l_redu.intros)
          apply(simp)
         apply(simp add: fresh_atm)
        apply(auto dest: fin_nrename2 simp add: fresh_prod fresh_atm)[1]
    (* LNot *)
       apply(drule sym)
       apply(drule nrename_Cut)
         apply(simp add: fresh_prod abs_fresh fresh_atm)
        apply(simp add: fresh_prod abs_fresh fresh_atm)
       apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
       apply(drule nrename_NotR)
        apply(simp add: fresh_prod abs_fresh fresh_atm)
       apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
       apply(drule nrename_NotL)
         apply(simp add: fresh_prod abs_fresh fresh_atm)
        apply(simp add: fresh_prod abs_fresh fresh_atm)
       apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
       apply(rule_tac x="Cut <b>.N'b (x).N'a" in exI)
       apply(simp add: fresh_atm)[1]
       apply(rule l_redu.intros)
            apply(auto simp add: fresh_prod fresh_atm intro: nrename_fresh_interesting1)[1]
           apply(auto simp add: fresh_atm fresh_prod intro: nrename_fresh_interesting1)[1]
          apply(auto simp add: fresh_atm fresh_prod intro: nrename_fresh_interesting2)[1]
         apply(auto simp add: fresh_atm fresh_prod intro: nrename_fresh_interesting2)[1]
        apply(simp add: fresh_atm)
       apply(simp add: fresh_atm)
    (* LAnd1 *)
      apply(auto dest: fin_crename simp add: fresh_prod fresh_atm)[1]
      apply(drule sym)
      apply(drule nrename_Cut)
        apply(simp add: fresh_prod abs_fresh fresh_atm)
       apply(simp add: fresh_prod abs_fresh fresh_atm)
      apply(auto)[1]
      apply(drule nrename_AndR)
        apply(simp add: fresh_prod abs_fresh fresh_atm)
       apply(simp add: fresh_prod abs_fresh fresh_atm)
      apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
      apply(drule nrename_AndL1)
        apply(simp add: fresh_prod abs_fresh fresh_atm)
       apply(simp add: fresh_prod abs_fresh fresh_atm)
      apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
      apply(rule_tac x="Cut <a1>.M'a (x).N'b" in exI)
      apply(simp add: fresh_atm)[1]
      apply(rule l_redu.intros)
           apply(auto simp add: fresh_atm abs_fresh fresh_prod intro: nrename_fresh_interesting2)[1]
          apply(auto simp add: abs_fresh fresh_atm fresh_prod intro: nrename_fresh_interesting1)[1]
         apply(auto simp add: fresh_atm fresh_prod intro: nrename_fresh_interesting1)[1]
        apply(auto simp add: fresh_atm fresh_prod intro: nrename_fresh_interesting1)[1]
       apply(auto simp add: fresh_atm fresh_prod intro: nrename_fresh_interesting1)[1]
      apply(simp add: fresh_atm)
    (* LAnd2 *)
     apply(auto dest: fin_crename simp add: fresh_prod fresh_atm)[1]
     apply(drule sym)
     apply(drule nrename_Cut)
       apply(simp add: fresh_prod abs_fresh fresh_atm)
      apply(simp add: fresh_prod abs_fresh fresh_atm)
     apply(auto)[1]
     apply(drule nrename_AndR)
       apply(simp add: fresh_prod abs_fresh fresh_atm)
      apply(simp add: fresh_prod abs_fresh fresh_atm)
     apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
     apply(drule nrename_AndL2)
       apply(simp add: fresh_prod abs_fresh fresh_atm)
      apply(simp add: fresh_prod abs_fresh fresh_atm)
     apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
     apply(rule_tac x="Cut <a2>.N'a (x).N'b" in exI)
     apply(simp add: fresh_atm)[1]
     apply(rule l_redu.intros)
          apply(auto simp add: fresh_atm abs_fresh fresh_prod intro: nrename_fresh_interesting2)[1]
         apply(auto simp add: abs_fresh fresh_atm fresh_prod intro: nrename_fresh_interesting1)[1]
        apply(auto simp add: fresh_atm fresh_prod intro: nrename_fresh_interesting1)[1]
       apply(auto simp add: fresh_atm fresh_prod intro: nrename_fresh_interesting1)[1]
      apply(auto simp add: fresh_atm fresh_prod intro: nrename_fresh_interesting1)[1]
     apply(simp add: fresh_atm)
    (* LOr1 *)
    apply(auto dest: fin_crename simp add: fresh_prod fresh_atm)[1]
    apply(drule sym)
    apply(drule nrename_Cut)
      apply(simp add: fresh_prod abs_fresh fresh_atm)
     apply(simp add: fresh_prod abs_fresh fresh_atm)
    apply(auto)[1]
    apply(drule nrename_OrL)
       apply(simp add: fresh_prod abs_fresh fresh_atm)
      apply(simp add: fresh_prod abs_fresh fresh_atm)
     apply(simp add: fresh_prod fresh_atm)
    apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
    apply(drule nrename_OrR1)
     apply(simp add: fresh_prod abs_fresh fresh_atm)
    apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
    apply(rule_tac x="Cut <a>.N' (x1).M'a" in exI)
    apply(rule conjI)
     apply(simp add: abs_fresh fresh_atm)[1]
    apply(rule l_redu.intros)
         apply(auto simp add: fresh_atm abs_fresh fresh_prod intro: nrename_fresh_interesting2)[1]
        apply(auto simp add: abs_fresh fresh_atm fresh_prod intro: nrename_fresh_interesting1)[1]
       apply(auto simp add: abs_fresh fresh_atm fresh_prod intro: nrename_fresh_interesting1)[1]
      apply(auto simp add: abs_fresh fresh_atm fresh_prod intro: nrename_fresh_interesting1)[1]
     apply(simp add: fresh_atm)
    apply(simp add: fresh_atm)
    (* LOr2 *)
   apply(auto dest: fin_crename simp add: fresh_prod fresh_atm)[1]
   apply(drule sym)
   apply(drule nrename_Cut)
     apply(simp add: fresh_prod abs_fresh fresh_atm)
    apply(simp add: fresh_prod abs_fresh fresh_atm)
   apply(auto)[1]
   apply(drule nrename_OrL)
      apply(simp add: fresh_prod abs_fresh fresh_atm)
     apply(simp add: fresh_prod abs_fresh fresh_atm)
    apply(simp add: fresh_prod fresh_atm)
   apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
   apply(drule nrename_OrR2)
    apply(simp add: fresh_prod abs_fresh fresh_atm)
   apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
   apply(rule_tac x="Cut <a>.N' (x2).N'a" in exI)
   apply(rule conjI)
    apply(simp add: abs_fresh fresh_atm)[1]
   apply(rule l_redu.intros)
        apply(auto simp add: fresh_atm abs_fresh fresh_prod intro: nrename_fresh_interesting2)[1]
       apply(auto simp add: abs_fresh fresh_atm fresh_prod intro: nrename_fresh_interesting1)[1]
      apply(auto simp add: abs_fresh fresh_atm fresh_prod intro: nrename_fresh_interesting1)[1]
     apply(auto simp add: abs_fresh fresh_atm fresh_prod intro: nrename_fresh_interesting1)[1]
    apply(simp add: fresh_atm)
   apply(simp add: fresh_atm)
    (* ImpL *)
  apply(auto dest: fin_crename simp add: fresh_prod fresh_atm)[1]
  apply(drule sym) 
  apply(drule nrename_Cut)
    apply(simp add: fresh_prod abs_fresh fresh_atm)
   apply(simp add: fresh_prod abs_fresh fresh_atm abs_supp fin_supp)
  apply(auto)[1]
  apply(drule nrename_ImpL)
     apply(simp add: fresh_prod abs_fresh fresh_atm)
    apply(simp add: fresh_prod abs_fresh fresh_atm)
   apply(simp add: fresh_prod fresh_atm)
  apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
  apply(drule nrename_ImpR)
    apply(simp add: fresh_prod abs_fresh fresh_atm)
   apply(simp add: fresh_prod abs_fresh fresh_atm)
  apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
  apply(rule_tac x="Cut <a>.(Cut <c>.M'a (x).N') (y).N'a" in exI)
  apply(rule conjI)
   apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
  apply(rule l_redu.intros)
       apply(auto simp add: fresh_atm abs_fresh abs_supp fin_supp fresh_prod intro: nrename_fresh_interesting1)[1]
      apply(auto simp add: abs_fresh fresh_atm abs_supp fin_supp fresh_prod intro: nrename_fresh_interesting2)[1]
     apply(auto simp add: abs_fresh fresh_atm abs_supp fin_supp fresh_prod intro: nrename_fresh_interesting1)[1]
    apply(auto simp add: abs_fresh fresh_atm abs_supp fin_supp fresh_prod intro: nrename_fresh_interesting2)[1]
   apply(auto simp add: abs_fresh fresh_atm abs_supp fin_supp fresh_prod intro: nrename_fresh_interesting2)[1]
  apply(auto simp add: abs_fresh fresh_atm abs_supp fin_supp fresh_prod intro: nrename_fresh_interesting2)[1]
  done

lemma nrename_aredu:
  assumes a: "(M[x⊢n>y]) ⟶⇩a M'" "x≠y"
  shows "∃M0. M0[x⊢n>y]=M' ∧ M ⟶⇩a M0"
  using a
  apply(nominal_induct "M[x⊢n>y]" M' avoiding: M x y rule: a_redu.strong_induct)
                  apply(drule  nrename_lredu)
                  apply(blast)
                 apply(drule  nrename_credu)
                 apply(blast)
    (* Cut *)
                apply(drule sym)
                apply(drule nrename_Cut)
                  apply(simp)
                 apply(simp)
                apply(auto)[1]
                apply(drule_tac x="M'a" in meta_spec)
                apply(drule_tac x="xa" in meta_spec)
                apply(drule_tac x="y" in meta_spec)
                apply(auto)[1]
                apply(rule_tac x="Cut <a>.M0 (x).N'" in exI)
                apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
                apply(rule conjI)
                 apply(rule trans)
                  apply(rule nrename.simps)
                   apply(drule nrename_fresh_interesting2)
                   apply(simp add: fresh_a_redu)
                  apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
                  apply(drule nrename_fresh_interesting1)
                   apply(simp add: fresh_prod fresh_atm)
                  apply(simp add: fresh_a_redu)
                 apply(simp)
                apply(auto)[1]
               apply(drule sym)
               apply(drule nrename_Cut)
                 apply(simp)
                apply(simp)
               apply(auto)[1]
               apply(drule_tac x="N'a" in meta_spec)
               apply(drule_tac x="xa" in meta_spec)
               apply(drule_tac x="y" in meta_spec)
               apply(auto)[1]
               apply(rule_tac x="Cut <a>.M' (x).M0" in exI)
               apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
               apply(rule conjI)
                apply(rule trans)
                 apply(rule nrename.simps)
                  apply(simp add: fresh_a_redu)
                 apply(simp add: abs_fresh abs_supp fin_supp fresh_atm fresh_prod)[1]
                apply(simp)
               apply(auto)[1]
    (* NotL *)
              apply(drule sym)
              apply(frule nrename_NotL_aux)
              apply(erule disjE)
               apply(auto)[1]
              apply(drule nrename_NotL')
                apply(simp)
               apply(simp add: fresh_atm)
              apply(erule disjE)
               apply(auto)[1]
               apply(drule_tac x="N'" in meta_spec)
               apply(drule_tac x="xa" in meta_spec)
               apply(drule_tac x="y" in meta_spec)
               apply(auto)[1]
               apply(rule_tac x="NotL <a>.M0 x" in exI)
               apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
               apply(auto)[1]
              apply(auto)[1]
              apply(drule_tac x="N'" in meta_spec)
              apply(drule_tac x="xa" in meta_spec)
              apply(drule_tac x="x" in meta_spec)
              apply(auto)[1]
              apply(rule_tac x="NotL <a>.M0 xa" in exI)
              apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
              apply(auto)[1]
    (* NotR *)
             apply(drule sym)
             apply(drule nrename_NotR)
              apply(simp)
             apply(auto)[1]
             apply(drule_tac x="N'" in meta_spec)
             apply(drule_tac x="xa" in meta_spec)
             apply(drule_tac x="y" in meta_spec)
             apply(auto)[1]
             apply(rule_tac x="NotR (x).M0 a" in exI)
             apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
             apply(auto)[1]
    (* AndR *)
            apply(drule sym)
            apply(drule nrename_AndR)
              apply(simp)
              apply(auto simp add: fresh_atm fresh_prod)[1]
             apply(auto simp add: fresh_atm fresh_prod)[1]
            apply(auto)[1]
            apply(drule_tac x="M'a" in meta_spec)
            apply(drule_tac x="x" in meta_spec)
            apply(drule_tac x="y" in meta_spec)
            apply(auto)[1]
            apply(rule_tac x="AndR <a>.M0 <b>.N' c" in exI)
            apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
            apply(auto)[1]
            apply(rule trans)
             apply(rule nrename.simps)
               apply(simp add: abs_fresh abs_supp fin_supp fresh_atm fresh_prod)[1]
              apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
              apply(auto intro: fresh_a_redu)[1]
             apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
            apply(simp)
           apply(drule sym)
           apply(drule nrename_AndR)
             apply(simp)
             apply(auto simp add: fresh_atm fresh_prod)[1]
            apply(auto simp add: fresh_atm fresh_prod)[1]
           apply(auto)[1]
           apply(drule_tac x="N'a" in meta_spec)
           apply(drule_tac x="x" in meta_spec)
           apply(drule_tac x="y" in meta_spec)
           apply(auto)[1]
           apply(rule_tac x="AndR <a>.M' <b>.M0 c" in exI)
           apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
           apply(auto)[1]
           apply(rule trans)
            apply(rule nrename.simps)
              apply(simp add: abs_fresh abs_supp fin_supp fresh_atm fresh_prod)[1]
              apply(auto intro: fresh_a_redu)[1]
             apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
            apply(simp)
           apply(simp)
    (* AndL1 *)
          apply(drule sym)
          apply(frule nrename_AndL1_aux)
          apply(erule disjE)
           apply(auto)[1]
          apply(drule nrename_AndL1')
            apply(simp)
           apply(simp add: fresh_atm)
          apply(erule disjE)
           apply(auto)[1]
           apply(drule_tac x="N'" in meta_spec)
           apply(drule_tac x="xa" in meta_spec)
           apply(drule_tac x="ya" in meta_spec)
           apply(auto)[1]
           apply(rule_tac x="AndL1 (x).M0 y" in exI)
           apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
           apply(auto)[1]
          apply(auto)[1]
          apply(drule_tac x="N'" in meta_spec)
          apply(drule_tac x="xa" in meta_spec)
          apply(drule_tac x="y" in meta_spec)
          apply(auto)[1]
          apply(rule_tac x="AndL1 (x).M0 xa" in exI)
          apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
          apply(auto)[1]
    (* AndL2 *)
         apply(drule sym)
         apply(frule nrename_AndL2_aux)
         apply(erule disjE)
          apply(auto)[1]
         apply(drule nrename_AndL2')
           apply(simp)
          apply(simp add: fresh_atm)
         apply(erule disjE)
          apply(auto)[1]
          apply(drule_tac x="N'" in meta_spec)
          apply(drule_tac x="xa" in meta_spec)
          apply(drule_tac x="ya" in meta_spec)
          apply(auto)[1]
          apply(rule_tac x="AndL2 (x).M0 y" in exI)
          apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
          apply(auto)[1]
         apply(auto)[1]
         apply(drule_tac x="N'" in meta_spec)
         apply(drule_tac x="xa" in meta_spec)
         apply(drule_tac x="y" in meta_spec)
         apply(auto)[1]
         apply(rule_tac x="AndL2 (x).M0 xa" in exI)
         apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
         apply(auto)[1]
    (* OrL *)
        apply(drule sym)
        apply(frule nrename_OrL_aux)
        apply(erule disjE)
         apply(auto)[1]
        apply(drule nrename_OrL')
           apply(simp add: fresh_prod fresh_atm)
          apply(simp add: fresh_atm)
         apply(simp add: fresh_atm)
        apply(erule disjE)
         apply(auto)[1]
         apply(drule_tac x="M'a" in meta_spec)
         apply(drule_tac x="xa" in meta_spec)
         apply(drule_tac x="ya" in meta_spec)
         apply(auto)[1]
         apply(rule_tac x="OrL (x).M0 (y).N' z" in exI)
         apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
         apply(auto)[1]
         apply(rule trans)
          apply(rule nrename.simps)
            apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
           apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
           apply(auto intro: fresh_a_redu)[1]
          apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
         apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
        apply(auto)[1]
        apply(drule_tac x="M'a" in meta_spec)
        apply(drule_tac x="xa" in meta_spec)
        apply(drule_tac x="z" in meta_spec)
        apply(auto)[1]
        apply(rule_tac x="OrL (x).M0 (y).N' xa" in exI)
        apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
        apply(auto)[1]
        apply(rule trans)
         apply(rule nrename.simps)
           apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
          apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
          apply(auto intro: fresh_a_redu)[1]
         apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
        apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
       apply(drule sym)
       apply(frule nrename_OrL_aux)
       apply(erule disjE)
        apply(auto)[1]
       apply(drule nrename_OrL')
          apply(simp add: fresh_prod fresh_atm)
         apply(simp add: fresh_atm)
        apply(simp add: fresh_atm)
       apply(erule disjE)
        apply(auto)[1]
        apply(drule_tac x="N'a" in meta_spec)
        apply(drule_tac x="xa" in meta_spec)
        apply(drule_tac x="ya" in meta_spec)
        apply(auto)[1]
        apply(rule_tac x="OrL (x).M' (y).M0 z" in exI)
        apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
        apply(auto)[1]
        apply(rule trans)
         apply(rule nrename.simps)
           apply(simp add: abs_fresh abs_supp fin_supp fresh_atm fresh_prod)[1]
           apply(auto intro: fresh_a_redu)[1]
          apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
         apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
        apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
       apply(auto)[1]
       apply(drule_tac x="N'a" in meta_spec)
       apply(drule_tac x="xa" in meta_spec)
       apply(drule_tac x="z" in meta_spec)
       apply(auto)[1]
       apply(rule_tac x="OrL (x).M' (y).M0 xa" in exI)
       apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
       apply(auto)[1]
       apply(rule trans)
        apply(rule nrename.simps)
          apply(simp add: abs_fresh abs_supp fin_supp fresh_atm fresh_prod)[1]
          apply(auto intro: fresh_a_redu)[1]
         apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
        apply(simp)
       apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
    (* OrR1 *)
      apply(drule sym)
      apply(drule nrename_OrR1)
       apply(simp)
      apply(auto)[1]
      apply(drule_tac x="N'" in meta_spec)
      apply(drule_tac x="x" in meta_spec)
      apply(drule_tac x="y" in meta_spec)
      apply(auto)[1]
      apply(rule_tac x="OrR1 <a>.M0 b" in exI)
      apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
      apply(auto)[1]
    (* OrR2 *)
     apply(drule sym)
     apply(drule nrename_OrR2)
      apply(simp)
     apply(auto)[1]
     apply(drule_tac x="N'" in meta_spec)
     apply(drule_tac x="x" in meta_spec)
     apply(drule_tac x="y" in meta_spec)
     apply(auto)[1]
     apply(rule_tac x="OrR2 <a>.M0 b" in exI)
     apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
     apply(auto)[1]
    (* ImpL *)
    apply(drule sym)
    apply(frule nrename_ImpL_aux)
    apply(erule disjE)
     apply(auto)[1]
    apply(drule nrename_ImpL')
       apply(simp add: fresh_prod fresh_atm)
      apply(simp add: fresh_atm)
     apply(simp add: fresh_atm)
    apply(erule disjE)
     apply(auto)[1]
     apply(drule_tac x="M'a" in meta_spec)
     apply(drule_tac x="xa" in meta_spec)
     apply(drule_tac x="ya" in meta_spec)
     apply(auto)[1]
     apply(rule_tac x="ImpL <a>.M0 (x).N' y" in exI)
     apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
     apply(auto)[1]
     apply(rule trans)
      apply(rule nrename.simps)
       apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
      apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
      apply(auto intro: fresh_a_redu)[1]
     apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
    apply(auto)[1]
    apply(drule_tac x="M'a" in meta_spec)
    apply(drule_tac x="xa" in meta_spec)
    apply(drule_tac x="y" in meta_spec)
    apply(auto)[1]
    apply(rule_tac x="ImpL <a>.M0 (x).N' xa" in exI)
    apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
    apply(auto)[1]
    apply(rule trans)
     apply(rule nrename.simps)
      apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
     apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
     apply(auto intro: fresh_a_redu)[1]
    apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
   apply(drule sym)
   apply(frule nrename_ImpL_aux)
   apply(erule disjE)
    apply(auto)[1]
   apply(drule nrename_ImpL')
      apply(simp add: fresh_prod fresh_atm)
     apply(simp add: fresh_atm)
    apply(simp add: fresh_atm)
   apply(erule disjE)
    apply(auto)[1]
    apply(drule_tac x="N'a" in meta_spec)
    apply(drule_tac x="xa" in meta_spec)
    apply(drule_tac x="ya" in meta_spec)
    apply(auto)[1]
    apply(rule_tac x="ImpL <a>.M' (x).M0 y" in exI)
    apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
    apply(auto)[1]
    apply(rule trans)
     apply(rule nrename.simps)
      apply(auto intro: fresh_a_redu)[1]
     apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
    apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
   apply(auto)[1]
   apply(drule_tac x="N'a" in meta_spec)
   apply(drule_tac x="xa" in meta_spec)
   apply(drule_tac x="y" in meta_spec)
   apply(auto)[1]
   apply(rule_tac x="ImpL <a>.M' (x).M0 xa" in exI)
   apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
   apply(auto)[1]
   apply(rule trans)
    apply(rule nrename.simps)
     apply(auto intro: fresh_a_redu)[1]
    apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
   apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
    (* ImpR *)
  apply(drule sym)
  apply(drule nrename_ImpR)
    apply(simp)
   apply(simp)
  apply(auto)[1]
  apply(drule_tac x="N'" in meta_spec)
  apply(drule_tac x="xa" in meta_spec)
  apply(drule_tac x="y" in meta_spec)
  apply(auto)[1]
  apply(rule_tac x="ImpR (x).<a>.M0 b" in exI)
  apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
  apply(auto)[1]
  done

lemma SNa_preserved_renaming2:
  assumes a: "SNa N"
  shows "SNa (N[x⊢n>y])"
  using a
  apply(induct rule: SNa_induct)
  apply(case_tac "x=y")
   apply(simp add: nrename_id)
  apply(rule SNaI)
  apply(drule nrename_aredu)
   apply(blast)+
  done

text ‹helper-stuff to set up the induction›

abbreviation
  SNa_set :: "trm set"
  where
    "SNa_set ≡ {M. SNa M}"

abbreviation
  A_Redu_set :: "(trm×trm) set"
  where
    "A_Redu_set ≡ {(N,M)| M N. M ⟶⇩a N}"

lemma SNa_elim:
  assumes a: "SNa M"
  shows "(∀M. (∀N. M ⟶⇩a N ⟶ P N)⟶ P M) ⟶ P M"
  using a
  by (induct rule: SNa.induct) (blast)

lemma wf_SNa_restricted:
  shows "wf (A_Redu_set ∩ (UNIV × SNa_set))"
  apply(unfold wf_def)
  apply(intro strip)
  apply(case_tac "SNa x")
   apply(simp (no_asm_use))
   apply(drule_tac P="P" in SNa_elim)
   apply(erule mp)
   apply(blast)
    (* other case *)
  apply(drule_tac x="x" in spec)
  apply(erule mp)
  apply(fast)
  done

definition SNa_Redu :: "(trm × trm) set" where
  "SNa_Redu ≡ A_Redu_set ∩ (UNIV × SNa_set)"

lemma wf_SNa_Redu:
  shows "wf SNa_Redu"
  apply(unfold SNa_Redu_def)
  apply(rule wf_SNa_restricted)
  done

lemma wf_measure_triple:
  shows "wf ((measure size) <*lex*> SNa_Redu <*lex*> SNa_Redu)"
  by (auto intro: wf_SNa_Redu)

lemma my_wf_induct_triple: 
  assumes a: " wf(r1 <*lex*> r2 <*lex*> r3)"           
    and     b: "⋀x. ⟦⋀y. ((fst y,fst (snd y),snd (snd y)),(fst x,fst (snd x), snd (snd x))) 
                                    ∈ (r1 <*lex*> r2 <*lex*> r3) ⟶ P y⟧ ⟹ P x"  
  shows "P x"
  using a
  apply(induct x rule: wf_induct_rule)
  apply(rule b)
  apply(simp)
  done

lemma my_wf_induct_triple': 
  assumes a: " wf(r1 <*lex*> r2 <*lex*> r3)"           
    and    b: "⋀x1 x2 x3. ⟦⋀y1 y2 y3. ((y1,y2,y3),(x1,x2,x3)) ∈ (r1 <*lex*> r2 <*lex*> r3) ⟶ P (y1,y2,y3)⟧ 
             ⟹ P (x1,x2,x3)"  
  shows "P (x1,x2,x3)"
  apply(rule_tac my_wf_induct_triple[OF a])
  apply(case_tac x rule: prod.exhaust)
  apply(simp)
  apply(rename_tac p a b)
  apply(case_tac b)
  apply(simp)
  apply(rule b)
  apply(blast)
  done

lemma my_wf_induct_triple'': 
  assumes a: " wf(r1 <*lex*> r2 <*lex*> r3)"           
    and     b: "⋀x1 x2 x3. ⟦⋀y1 y2 y3. ((y1,y2,y3),(x1,x2,x3)) ∈ (r1 <*lex*> r2 <*lex*> r3) ⟶ P y1 y2 y3⟧
               ⟹ P x1 x2 x3"  
  shows "P x1 x2 x3"
  apply(rule_tac my_wf_induct_triple'[where P="λ(x1,x2,x3). P x1 x2 x3", simplified])
   apply(rule a)
  apply(rule b)
  apply(auto)
  done

lemma excluded_m:
  assumes a: "<a>:M ∈ (∥<B>∥)" "(x):N ∈ (∥(B)∥)"
  shows "(<a>:M ∈ BINDINGc B (∥(B)∥) ∨ (x):N ∈ BINDINGn B (∥<B>∥))
      ∨¬(<a>:M ∈ BINDINGc B (∥(B)∥) ∨ (x):N ∈ BINDINGn B (∥<B>∥))"
  by (blast)

text ‹The following two simplification rules are necessary because of the 
      new definition of lexicographic ordering›
lemma ne_and_SNa_Redu[simp]: "M ≠ x ∧ (M,x) ∈ SNa_Redu ⟷ (M,x) ∈ SNa_Redu"
  using wf_SNa_Redu by auto

lemma ne_and_less_size [simp]: "A ≠ B ∧ size A < size B ⟷ size A < size B"
  by auto

lemma tricky_subst:
  assumes a1: "b♯(c,N)"
    and     a2: "z♯(x,P)"
    and     a3: "M≠Ax z b"
  shows "(Cut <c>.N (z).M){b:=(x).P} = Cut <c>.N (z).(M{b:=(x).P})"
  using a1 a2 a3
  apply -
  apply(generate_fresh "coname")
  apply(subgoal_tac "Cut <c>.N (z).M = Cut <ca>.([(ca,c)]∙N) (z).M")
   apply(simp)
   apply(rule trans)
    apply(rule better_Cut_substc)
     apply(simp)
    apply(simp add: abs_fresh)
   apply(simp)
   apply(subgoal_tac "b♯([(ca,c)]∙N)")
    apply(simp add: forget)
    apply(simp add: trm.inject)
   apply(simp add: fresh_left calc_atm fresh_prod fresh_atm)
  apply(simp add: trm.inject)
  apply(rule sym)
  apply(simp add: alpha fresh_prod fresh_atm)
  done

text ‹3rd lemma›

lemma CUT_SNa_aux:
  assumes a1: "<a>:M ∈ (∥<B>∥)"
    and     a2: "SNa M"
    and     a3: "(x):N ∈ (∥(B)∥)"
    and     a4: "SNa N"
  shows   "SNa (Cut <a>.M (x).N)"
  using a1 a2 a3 a4 [[simproc del: defined_all]]
  apply(induct B M N arbitrary: a x rule: my_wf_induct_triple''[OF wf_measure_triple])
  apply(rule SNaI)
  apply(drule Cut_a_redu_elim)
  apply(erule disjE)
    (* left-inner reduction *)
   apply(erule exE)
   apply(erule conjE)+
   apply(simp)
   apply(drule_tac x="x1" in meta_spec)
   apply(drule_tac x="M'a" in meta_spec)
   apply(drule_tac x="x3" in meta_spec)
   apply(drule conjunct2)
   apply(drule mp)
    apply(rule conjI)
     apply(simp)
    apply(rule disjI1)
    apply(simp add: SNa_Redu_def)
   apply(drule_tac x="a" in spec)
   apply(drule mp)
    apply(simp add: CANDs_preserved_single)
   apply(drule mp)
    apply(simp add: a_preserves_SNa)
   apply(drule_tac x="x" in spec)
   apply(simp)
  apply(erule disjE)
    (* right-inner reduction *)
   apply(erule exE)
   apply(erule conjE)+
   apply(simp)
   apply(drule_tac x="x1" in meta_spec)
   apply(drule_tac x="x2" in meta_spec)
   apply(drule_tac x="N'" in meta_spec)
   apply(drule conjunct2)
   apply(drule mp)
    apply(rule conjI)
     apply(simp)
    apply(rule disjI2)
    apply(simp add: SNa_Redu_def)
   apply(drule_tac x="a" in spec)
   apply(drule mp)
    apply(simp add: CANDs_preserved_single)
   apply(drule mp)
    apply(assumption)
   apply(drule_tac x="x" in spec)
   apply(drule mp)
    apply(simp add: CANDs_preserved_single)
   apply(drule mp)
    apply(simp add: a_preserves_SNa)
   apply(assumption)
  apply(erule disjE)
    (******** c-reduction *********)
   apply(drule Cut_c_redu_elim)
    (* c-left reduction*)
   apply(erule disjE)
    apply(erule conjE)
    apply(frule_tac B="x1" in fic_CANDS)
     apply(simp)
    apply(erule disjE)
    (* in AXIOMSc *)
     apply(simp add: AXIOMSc_def)
     apply(erule exE)+
     apply(simp add: ctrm.inject)
     apply(simp add: alpha)
     apply(erule disjE)
      apply(simp)
      apply(rule impI)
      apply(simp)
      apply(subgoal_tac "fic (Ax y b) b")(*A*)
       apply(simp)
    (*A*)
      apply(auto)[1]
     apply(simp)
     apply(rule impI)
     apply(simp)
     apply(subgoal_tac "fic (Ax ([(a,aa)]∙y) a) a")(*B*)
      apply(simp)
    (*B*)
     apply(auto)[1]
    (* in BINDINGc *)
    apply(simp)
    apply(drule BINDINGc_elim)
    apply(simp)
    (* c-right reduction*)
   apply(erule conjE)
   apply(frule_tac B="x1" in fin_CANDS)
    apply(simp)
   apply(erule disjE)
    (* in AXIOMSc *)
    apply(simp add: AXIOMSn_def)
    apply(erule exE)+
    apply(simp add: ntrm.inject)
    apply(simp add: alpha)
    apply(erule disjE)
     apply(simp)
     apply(rule impI)
     apply(simp)
     apply(subgoal_tac "fin (Ax xa b) xa")(*A*)
      apply(simp)
    (*A*)
     apply(auto)[1]
    apply(simp)
    apply(rule impI)
    apply(simp)
    apply(subgoal_tac "fin (Ax x ([(x,xa)]∙b)) x")(*B*)
     apply(simp)
    (*B*)
    apply(auto)[1]
    (* in BINDINGc *)
   apply(simp)
   apply(drule BINDINGn_elim)
   apply(simp)
    (*********** l-reductions ************)
  apply(drule Cut_l_redu_elim)
  apply(erule disjE)
    (* ax1 *)
   apply(erule exE)
   apply(simp)
   apply(simp add: SNa_preserved_renaming1)
  apply(erule disjE)
    (* ax2 *)
   apply(erule exE)
   apply(simp add: SNa_preserved_renaming2)
  apply(erule disjE)
    (* LNot *)
   apply(erule exE)+
   apply(auto)[1]
   apply(frule_tac excluded_m)
    apply(assumption)
   apply(erule disjE)
    (* one of them in BINDING *)
    apply(erule disjE)
     apply(drule fin_elims)
     apply(drule fic_elims)
     apply(simp)
     apply(drule BINDINGc_elim)
     apply(drule_tac x="x" in spec)
     apply(drule_tac x="NotL <b>.N' x" in spec)
     apply(simp)
     apply(simp add: better_NotR_substc)
     apply(generate_fresh "coname")
     apply(subgoal_tac "fresh_fun (λa'. Cut <a'>.NotR (y).M'a a' (x).NotL <b>.N' x) 
                   =  Cut <c>.NotR (y).M'a c (x).NotL <b>.N' x")
      apply(simp)
      apply(subgoal_tac "Cut <c>.NotR (y).M'a c (x).NotL <b>.N' x ⟶⇩a Cut <b>.N' (y).M'a")
       apply(simp only: a_preserves_SNa)
      apply(rule al_redu)
      apply(rule better_LNot_intro)
       apply(simp)
      apply(simp)
     apply(fresh_fun_simp (no_asm))
     apply(simp)
    (* other case of in BINDING *)
    apply(drule fin_elims)
    apply(drule fic_elims)
    apply(simp)
    apply(drule BINDINGn_elim)
    apply(drule_tac x="a" in spec)
    apply(drule_tac x="NotR (y).M'a a" in spec)
    apply(simp)
    apply(simp add: better_NotL_substn)
    apply(generate_fresh "name")
    apply(subgoal_tac "fresh_fun (λx'. Cut <a>.NotR (y).M'a a (x').NotL <b>.N' x') 
                   = Cut <a>.NotR (y).M'a a (c).NotL <b>.N' c")
     apply(simp)
     apply(subgoal_tac "Cut <a>.NotR (y).M'a a (c).NotL <b>.N' c ⟶⇩a Cut <b>.N' (y).M'a")
      apply(simp only: a_preserves_SNa)
     apply(rule al_redu)
     apply(rule better_LNot_intro)
      apply(simp)
     apply(simp)
    apply(fresh_fun_simp (no_asm))
    apply(simp)
    (* none of them in BINDING *)
   apply(simp)
   apply(erule conjE)
   apply(frule CAND_NotR_elim)
    apply(assumption)
   apply(erule exE)
   apply(frule CAND_NotL_elim)
    apply(assumption)
   apply(erule exE)
   apply(simp only: ty.inject)
   apply(drule_tac x="B'" in meta_spec)
   apply(drule_tac x="N'" in meta_spec)
   apply(drule_tac x="M'a" in meta_spec)
   apply(erule conjE)+
   apply(drule mp)
    apply(simp)
   apply(drule_tac x="b" in spec)
   apply(rotate_tac 13)
   apply(drule mp)
    apply(assumption)
   apply(rotate_tac 13)
   apply(drule mp)
    apply(simp add: CANDs_imply_SNa)
   apply(drule_tac x="y" in spec)
   apply(rotate_tac 13)
   apply(drule mp)
    apply(assumption)
   apply(rotate_tac 13)
   apply(drule mp)
    apply(simp add: CANDs_imply_SNa)
   apply(assumption)
    (* LAnd1 case *)
  apply(erule disjE)
   apply(erule exE)+
   apply(auto)[1]
   apply(frule_tac excluded_m)
    apply(assumption)
   apply(erule disjE)
    (* one of them in BINDING *)
    apply(erule disjE)
     apply(drule fin_elims)
     apply(drule fic_elims)
     apply(simp)
     apply(drule BINDINGc_elim)
     apply(drule_tac x="x" in spec)
     apply(drule_tac x="AndL1 (y).N' x" in spec)
     apply(simp)
     apply(simp add: better_AndR_substc)
     apply(generate_fresh "coname")
     apply(subgoal_tac "fresh_fun (λa'. Cut <a'>.AndR <b>.M1 <c>.M2 a' (x).AndL1 (y).N' x) 
                   = Cut <ca>.AndR <b>.M1 <c>.M2 ca (x).AndL1 (y).N' x")
      apply(simp)
      apply(subgoal_tac "Cut <ca>.AndR <b>.M1 <c>.M2 ca (x).AndL1 (y).N' x ⟶⇩a Cut <b>.M1 (y).N'")
       apply(auto intro: a_preserves_SNa)[1]
      apply(rule al_redu)
      apply(rule better_LAnd1_intro)
       apply(simp add: abs_fresh fresh_prod fresh_atm)
      apply(simp)
     apply(fresh_fun_simp (no_asm))
     apply(simp)
    (* other case of in BINDING *)
    apply(drule fin_elims)
    apply(drule fic_elims)
    apply(simp)
    apply(drule BINDINGn_elim)
    apply(drule_tac x="a" in spec)
    apply(drule_tac x="AndR <b>.M1 <c>.M2 a" in spec)
    apply(simp)
    apply(simp add: better_AndL1_substn)
    apply(generate_fresh "name")
    apply(subgoal_tac "fresh_fun (λz'. Cut <a>.AndR <b>.M1 <c>.M2 a (z').AndL1 (y).N' z') 
                   = Cut <a>.AndR <b>.M1 <c>.M2 a (ca).AndL1 (y).N' ca")
     apply(simp)
     apply(subgoal_tac "Cut <a>.AndR <b>.M1 <c>.M2 a (ca).AndL1 (y).N' ca ⟶⇩a Cut <b>.M1 (y).N'")
      apply(auto intro: a_preserves_SNa)[1]
     apply(rule al_redu)
     apply(rule better_LAnd1_intro)
      apply(simp add: abs_fresh fresh_prod fresh_atm) 
     apply(simp add: abs_fresh fresh_prod fresh_atm)
    apply(fresh_fun_simp (no_asm))
    apply(simp)
    (* none of them in BINDING *)
   apply(simp)
   apply(erule conjE)
   apply(frule CAND_AndR_elim)
    apply(assumption)
   apply(erule exE)
   apply(frule CAND_AndL1_elim)
    apply(assumption)
   apply(erule exE)+
   apply(simp only: ty.inject)
   apply(drule_tac x="B1" in meta_spec)
   apply(drule_tac x="M1" in meta_spec)
   apply(drule_tac x="N'" in meta_spec)
   apply(erule conjE)+
   apply(drule mp)
    apply(simp)
   apply(drule_tac x="b" in spec)
   apply(rotate_tac 14)
   apply(drule mp)
    apply(assumption)
   apply(rotate_tac 14)
   apply(drule mp)
    apply(simp add: CANDs_imply_SNa)
   apply(drule_tac x="y" in spec)
   apply(rotate_tac 15)
   apply(drule mp)
    apply(assumption)
   apply(rotate_tac 15)
   apply(drule mp)
    apply(simp add: CANDs_imply_SNa)
   apply(assumption)
    (* LAnd2 case *)
  apply(erule disjE)
   apply(erule exE)+
   apply(auto)[1]
   apply(frule_tac excluded_m)
    apply(assumption)
   apply(erule disjE)
    (* one of them in BINDING *)
    apply(erule disjE)
     apply(drule fin_elims)
     apply(drule fic_elims)
     apply(simp)
     apply(drule BINDINGc_elim)
     apply(drule_tac x="x" in spec)
     apply(drule_tac x="AndL2 (y).N' x" in spec)
     apply(simp)
     apply(simp add: better_AndR_substc)
     apply(generate_fresh "coname")
     apply(subgoal_tac "fresh_fun (λa'. Cut <a'>.AndR <b>.M1 <c>.M2 a' (x).AndL2 (y).N' x) 
                   = Cut <ca>.AndR <b>.M1 <c>.M2 ca (x).AndL2 (y).N' x")
      apply(simp)
      apply(subgoal_tac "Cut <ca>.AndR <b>.M1 <c>.M2 ca (x).AndL2 (y).N' x ⟶⇩a Cut <c>.M2 (y).N'")
       apply(auto intro: a_preserves_SNa)[1]
      apply(rule al_redu)
      apply(rule better_LAnd2_intro)
       apply(simp add: abs_fresh fresh_prod fresh_atm)
      apply(simp)
     apply(fresh_fun_simp (no_asm))
     apply(simp)
    (* other case of in BINDING *)
    apply(drule fin_elims)
    apply(drule fic_elims)
    apply(simp)
    apply(drule BINDINGn_elim)
    apply(drule_tac x="a" in spec)
    apply(drule_tac x="AndR <b>.M1 <c>.M2 a" in spec)
    apply(simp)
    apply(simp add: better_AndL2_substn)
    apply(generate_fresh "name")
    apply(subgoal_tac "fresh_fun (λz'. Cut <a>.AndR <b>.M1 <c>.M2 a (z').AndL2 (y).N' z') 
                   = Cut <a>.AndR <b>.M1 <c>.M2 a (ca).AndL2 (y).N' ca")
     apply(simp)
     apply(subgoal_tac "Cut <a>.AndR <b>.M1 <c>.M2 a (ca).AndL2 (y).N' ca ⟶⇩a Cut <c>.M2 (y).N'")
      apply(auto intro: a_preserves_SNa)[1]
     apply(rule al_redu)
     apply(rule better_LAnd2_intro)
      apply(simp add: abs_fresh fresh_prod fresh_atm) 
     apply(simp add: abs_fresh fresh_prod fresh_atm)
    apply(fresh_fun_simp (no_asm))
    apply(simp)
    (* none of them in BINDING *)
   apply(simp)
   apply(erule conjE)
   apply(frule CAND_AndR_elim)
    apply(assumption)
   apply(erule exE)
   apply(frule CAND_AndL2_elim)
    apply(assumption)
   apply(erule exE)+
   apply(simp only: ty.inject)
   apply(drule_tac x="B2" in meta_spec)
   apply(drule_tac x="M2" in meta_spec)
   apply(drule_tac x="N'" in meta_spec)
   apply(erule conjE)+
   apply(drule mp)
    apply(simp)
   apply(drule_tac x="c" in spec)
   apply(rotate_tac 14)
   apply(drule mp)
    apply(assumption)
   apply(rotate_tac 14)
   apply(drule mp)
    apply(simp add: CANDs_imply_SNa)
   apply(drule_tac x="y" in spec)
   apply(rotate_tac 15)
   apply(drule mp)
    apply(assumption)
   apply(rotate_tac 15)
   apply(drule mp)
    apply(simp add: CANDs_imply_SNa)
   apply(assumption)
    (* LOr1 case *)
  apply(erule disjE)
   apply(erule exE)+
   apply(auto)[1]
   apply(frule_tac excluded_m)
    apply(assumption)
   apply(erule disjE)
    (* one of them in BINDING *)
    apply(erule disjE)
     apply(drule fin_elims)
     apply(drule fic_elims)
     apply(simp)
     apply(drule BINDINGc_elim)
     apply(drule_tac x="x" in spec)
     apply(drule_tac x="OrL (z).M1 (y).M2 x" in spec)
     apply(simp)
     apply(simp add: better_OrR1_substc)
     apply(generate_fresh "coname")
     apply(subgoal_tac "fresh_fun (λa'. Cut <a'>.OrR1 <b>.N' a' (x).OrL (z).M1 (y).M2 x) 
                   = Cut <c>.OrR1 <b>.N' c (x).OrL (z).M1 (y).M2 x")
      apply(simp)
      apply(subgoal_tac "Cut <c>.OrR1 <b>.N' c (x).OrL (z).M1 (y).M2 x ⟶⇩a Cut <b>.N' (z).M1")
       apply(auto intro: a_preserves_SNa)[1]
      apply(rule al_redu)
      apply(rule better_LOr1_intro)
       apply(simp add: abs_fresh fresh_prod fresh_atm)
      apply(simp add: abs_fresh)
     apply(fresh_fun_simp (no_asm))
     apply(simp)
    (* other case of in BINDING *)
    apply(drule fin_elims)
    apply(drule fic_elims)
    apply(simp)
    apply(drule BINDINGn_elim)
    apply(drule_tac x="a" in spec)
    apply(drule_tac x="OrR1 <b>.N' a" in spec)
    apply(simp)
    apply(simp add: better_OrL_substn)
    apply(generate_fresh "name")
    apply(subgoal_tac "fresh_fun (λz'. Cut <a>.OrR1 <b>.N' a (z').OrL (z).M1 (y).M2 z') 
                   = Cut <a>.OrR1 <b>.N' a (c).OrL (z).M1 (y).M2 c")
     apply(simp)
     apply(subgoal_tac "Cut <a>.OrR1 <b>.N' a (c).OrL (z).M1 (y).M2 c ⟶⇩a Cut <b>.N' (z).M1")
      apply(auto intro: a_preserves_SNa)[1]
     apply(rule al_redu)
     apply(rule better_LOr1_intro)
      apply(simp add: abs_fresh fresh_prod fresh_atm) 
     apply(simp add: abs_fresh fresh_prod fresh_atm)
    apply(fresh_fun_simp (no_asm))
    apply(simp)
    (* none of them in BINDING *)
   apply(simp)
   apply(erule conjE)
   apply(frule CAND_OrR1_elim)
    apply(assumption)
   apply(erule exE)+
   apply(frule CAND_OrL_elim)
    apply(assumption)
   apply(erule exE)+
   apply(simp only: ty.inject)
   apply(drule_tac x="B1" in meta_spec)
   apply(drule_tac x="N'" in meta_spec)
   apply(drule_tac x="M1" in meta_spec)
   apply(erule conjE)+
   apply(drule mp)
    apply(simp)
   apply(drule_tac x="b" in spec)
   apply(rotate_tac 15)
   apply(drule mp)
    apply(assumption)
   apply(rotate_tac 15)
   apply(drule mp)
    apply(simp add: CANDs_imply_SNa)
   apply(drule_tac x="z" in spec)
   apply(rotate_tac 15)
   apply(drule mp)
    apply(assumption)
   apply(rotate_tac 15)
   apply(drule mp)
    apply(simp add: CANDs_imply_SNa)
   apply(assumption)
    (* LOr2 case *)
  apply(erule disjE)
   apply(erule exE)+
   apply(auto)[1]
   apply(frule_tac excluded_m)
    apply(assumption)
   apply(erule disjE)
    (* one of them in BINDING *)
    apply(erule disjE)
     apply(drule fin_elims)
     apply(drule fic_elims)
     apply(simp)
     apply(drule BINDINGc_elim)
     apply(drule_tac x="x" in spec)
     apply(drule_tac x="OrL (z).M1 (y).M2 x" in spec)
     apply(simp)
     apply(simp add: better_OrR2_substc)
     apply(generate_fresh "coname")
     apply(subgoal_tac "fresh_fun (λa'. Cut <a'>.OrR2 <b>.N' a' (x).OrL (z).M1 (y).M2 x) 
                   = Cut <c>.OrR2 <b>.N' c (x).OrL (z).M1 (y).M2 x")
      apply(simp)
      apply(subgoal_tac "Cut <c>.OrR2 <b>.N' c (x).OrL (z).M1 (y).M2 x ⟶⇩a Cut <b>.N' (y).M2")
       apply(auto intro: a_preserves_SNa)[1]
      apply(rule al_redu)
      apply(rule better_LOr2_intro)
       apply(simp add: abs_fresh fresh_prod fresh_atm)
      apply(simp add: abs_fresh)
     apply(fresh_fun_simp (no_asm))
     apply(simp)
    (* other case of in BINDING *)
    apply(drule fin_elims)
    apply(drule fic_elims)
    apply(simp)
    apply(drule BINDINGn_elim)
    apply(drule_tac x="a" in spec)
    apply(drule_tac x="OrR2 <b>.N' a" in spec)
    apply(simp)
    apply(simp add: better_OrL_substn)
    apply(generate_fresh "name")
    apply(subgoal_tac "fresh_fun (λz'. Cut <a>.OrR2 <b>.N' a (z').OrL (z).M1 (y).M2 z') 
                   = Cut <a>.OrR2 <b>.N' a (c).OrL (z).M1 (y).M2 c")
     apply(simp)
     apply(subgoal_tac "Cut <a>.OrR2 <b>.N' a (c).OrL (z).M1 (y).M2 c ⟶⇩a Cut <b>.N' (y).M2")
      apply(auto intro: a_preserves_SNa)[1]
     apply(rule al_redu)
     apply(rule better_LOr2_intro)
      apply(simp add: abs_fresh fresh_prod fresh_atm) 
     apply(simp add: abs_fresh fresh_prod fresh_atm)
    apply(fresh_fun_simp (no_asm))
    apply(simp)
    (* none of them in BINDING *)
   apply(simp)
   apply(erule conjE)
   apply(frule CAND_OrR2_elim)
    apply(assumption)
   apply(erule exE)+
   apply(frule CAND_OrL_elim)
    apply(assumption)
   apply(erule exE)+
   apply(simp only: ty.inject)
   apply(drule_tac x="B2" in meta_spec)
   apply(drule_tac x="N'" in meta_spec)
   apply(drule_tac x="M2" in meta_spec)
   apply(erule conjE)+
   apply(drule mp)
    apply(simp)
   apply(drule_tac x="b" in spec)
   apply(rotate_tac 15)
   apply(drule mp)
    apply(assumption)
   apply(rotate_tac 15)
   apply(drule mp)
    apply(simp add: CANDs_imply_SNa)
   apply(drule_tac x="y" in spec)
   apply(rotate_tac 15)
   apply(drule mp)
    apply(assumption)
   apply(rotate_tac 15)
   apply(drule mp)
    apply(simp add: CANDs_imply_SNa)
   apply(assumption)
    (* LImp case *)
  apply(erule exE)+
  apply(auto)[1]
  apply(frule_tac excluded_m)
   apply(assumption)
  apply(erule disjE)
    (* one of them in BINDING *)
   apply(erule disjE)
    apply(drule fin_elims)
    apply(drule fic_elims)
    apply(simp)
    apply(drule BINDINGc_elim)
    apply(drule_tac x="x" in spec)
    apply(drule_tac x="ImpL <c>.N1 (y).N2 x" in spec)
    apply(simp)
    apply(simp add: better_ImpR_substc)
    apply(generate_fresh "coname")
    apply(subgoal_tac "fresh_fun (λa'. Cut <a'>.ImpR (z).<b>.M'a a' (x).ImpL <c>.N1 (y).N2 x)
                   = Cut <ca>.ImpR (z).<b>.M'a ca (x).ImpL <c>.N1 (y).N2 x")
     apply(simp)
     apply(subgoal_tac "Cut <ca>.ImpR (z).<b>.M'a ca (x).ImpL <c>.N1 (y).N2 x ⟶⇩a 
                                                          Cut <b>.Cut <c>.N1 (z).M'a (y).N2")
      apply(auto intro: a_preserves_SNa)[1]
     apply(rule al_redu)
     apply(rule better_LImp_intro)
       apply(simp add: abs_fresh fresh_prod fresh_atm)
      apply(simp add: abs_fresh)
     apply(simp)
    apply(fresh_fun_simp (no_asm))
    apply(simp)
    (* other case of in BINDING *)
   apply(drule fin_elims)
   apply(drule fic_elims)
   apply(simp)
   apply(drule BINDINGn_elim)
   apply(drule_tac x="a" in spec)
   apply(drule_tac x="ImpR (z).<b>.M'a a" in spec)
   apply(simp)
   apply(simp add: better_ImpL_substn)
   apply(generate_fresh "name")
   apply(subgoal_tac "fresh_fun (λz'. Cut <a>.ImpR (z).<b>.M'a a (z').ImpL <c>.N1 (y).N2 z')
                   = Cut <a>.ImpR (z).<b>.M'a a (ca).ImpL <c>.N1 (y).N2 ca")
    apply(simp)
    apply(subgoal_tac "Cut <a>.ImpR (z).<b>.M'a a (ca).ImpL <c>.N1 (y).N2 ca ⟶⇩a 
                                                          Cut <b>.Cut <c>.N1 (z).M'a (y).N2")
     apply(auto intro: a_preserves_SNa)[1]
    apply(rule al_redu)
    apply(rule better_LImp_intro)
      apply(simp add: abs_fresh fresh_prod fresh_atm) 
     apply(simp add: abs_fresh fresh_prod fresh_atm)
    apply(simp)
   apply(fresh_fun_simp (no_asm))
    apply(simp add: abs_fresh abs_supp fin_supp)
   apply(simp add: abs_fresh abs_supp fin_supp)
  apply(simp)
    (* none of them in BINDING *)
  apply(erule conjE)
  apply(frule CAND_ImpL_elim)
   apply(assumption)
  apply(erule exE)+
  apply(frule CAND_ImpR_elim) (* check here *)
   apply(assumption)
  apply(erule exE)+
  apply(erule conjE)+
  apply(simp only: ty.inject)
  apply(erule conjE)+
  apply(case_tac "M'a=Ax z b")
    (* case Ma = Ax z b *)
   apply(rule_tac t="Cut <b>.(Cut <c>.N1 (z).M'a) (y).N2" and s="Cut <b>.(M'a{z:=<c>.N1}) (y).N2" in subst)
    apply(simp)
   apply(drule_tac x="c" in spec)
   apply(drule_tac x="N1" in spec)
   apply(drule mp)
    apply(simp)
   apply(drule_tac x="B2" in meta_spec)
   apply(drule_tac x="M'a{z:=<c>.N1}" in meta_spec)
   apply(drule_tac x="N2" in meta_spec)
   apply(drule conjunct1)
   apply(drule mp)
    apply(simp)
   apply(rotate_tac 17)
   apply(drule_tac x="b" in spec)
   apply(drule mp)
    apply(assumption)
   apply(drule mp)
    apply(simp add: CANDs_imply_SNa)
   apply(rotate_tac 17)
   apply(drule_tac x="y" in spec)
   apply(drule mp)
    apply(assumption)
   apply(drule mp)
    apply(simp add: CANDs_imply_SNa)
   apply(assumption)
    (* case Ma ≠ Ax z b *)
  apply(subgoal_tac "<b>:Cut <c>.N1 (z).M'a ∈ ∥<B2>∥") (* lemma *)
   apply(frule_tac meta_spec)
   apply(drule_tac x="B2" in meta_spec)
   apply(drule_tac x="Cut <c>.N1 (z).M'a" in meta_spec)
   apply(drule_tac x="N2" in meta_spec)
   apply(erule conjE)+
   apply(drule mp)
    apply(simp)
   apply(rotate_tac 20)
   apply(drule_tac x="b" in spec)
   apply(rotate_tac 20)
   apply(drule mp)
    apply(assumption)
   apply(rotate_tac 20)
   apply(drule mp)
    apply(simp add: CANDs_imply_SNa)
   apply(rotate_tac 20)
   apply(drule_tac x="y" in spec)
   apply(rotate_tac 20)
   apply(drule mp)
    apply(assumption)
   apply(rotate_tac 20)
   apply(drule mp)
    apply(simp add: CANDs_imply_SNa)
   apply(assumption)
    (* lemma *)
  apply(subgoal_tac "<b>:Cut <c>.N1 (z).M'a ∈ BINDINGc B2 (∥(B2)∥)") (* second lemma *)
   apply(simp add: BINDING_implies_CAND)
    (* second lemma *)
  apply(simp (no_asm) add: BINDINGc_def)
  apply(rule exI)+
  apply(rule conjI)
   apply(rule refl)
  apply(rule allI)+
  apply(rule impI)
  apply(generate_fresh "name")
  apply(rule_tac t="Cut <c>.N1 (z).M'a" and s="Cut <c>.N1 (ca).([(ca,z)]∙M'a)" in subst)
   apply(simp add: trm.inject alpha fresh_prod fresh_atm)
  apply(rule_tac t="(Cut <c>.N1 (ca).([(ca,z)]∙M'a)){b:=(xa).P}" 
      and s="Cut <c>.N1 (ca).(([(ca,z)]∙M'a){b:=(xa).P})" in subst)
   apply(rule sym)
   apply(rule tricky_subst)
     apply(simp)
    apply(simp)
   apply(clarify)
   apply(drule pt_bij1[OF pt_name_inst, OF at_name_inst])
   apply(simp add: calc_atm)
  apply(drule_tac x="B1" in meta_spec)
  apply(drule_tac x="N1" in meta_spec)
  apply(drule_tac x="([(ca,z)]∙M'a){b:=(xa).P}" in meta_spec)
  apply(drule conjunct1)
  apply(drule mp)
   apply(simp)
  apply(rotate_tac 19)
  apply(drule_tac x="c" in spec)
  apply(drule mp)
   apply(assumption)
  apply(drule mp)
   apply(simp add: CANDs_imply_SNa)
  apply(rotate_tac 19)
  apply(drule_tac x="ca" in spec)
  apply(subgoal_tac "(ca):([(ca,z)]∙M'a){b:=(xa).P} ∈ ∥(B1)∥")(*A*)
   apply(drule mp)
    apply(assumption)
   apply(drule mp)
    apply(simp add: CANDs_imply_SNa)
   apply(assumption)
    (*A*)
  apply(drule_tac x="[(ca,z)]∙xa" in spec)
  apply(drule_tac x="[(ca,z)]∙P" in spec)
  apply(rotate_tac 19)
  apply(simp add: fresh_prod fresh_left)
  apply(drule mp)
   apply(rule conjI)
    apply(auto simp add: calc_atm)[1]
   apply(rule conjI)
    apply(auto simp add: calc_atm)[1]
   apply(drule_tac pi="[(ca,z)]" and x="(xa):P" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
   apply(simp add: CAND_eqvt_name)
  apply(drule_tac pi="[(ca,z)]" and X="∥(B1)∥" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
  apply(simp add: CAND_eqvt_name csubst_eqvt)
  apply(perm_simp)
  done


(* parallel substitution *)


lemma CUT_SNa:
  assumes a1: "<a>:M ∈ (∥<B>∥)"
    and     a2: "(x):N ∈ (∥(B)∥)"
  shows   "SNa (Cut <a>.M (x).N)"
  using a1 a2
  apply -
  apply(rule CUT_SNa_aux[OF a1])
    apply(simp_all add: CANDs_imply_SNa)
  done 


fun 
  findn :: "(name×coname×trm) list⇒name⇒(coname×trm) option"
  where
    "findn [] x = None"
  | "findn ((y,c,P)#θ_n) x = (if y=x then Some (c,P) else findn θ_n x)"

lemma findn_eqvt[eqvt]:
  fixes pi1::"name prm"
    and   pi2::"coname prm"
  shows "(pi1∙findn θ_n x) = findn (pi1∙θ_n) (pi1∙x)" 
    and   "(pi2∙findn θ_n x) = findn (pi2∙θ_n) (pi2∙x)"
   apply(induct θ_n)
     apply(auto simp add: perm_bij) 
  done

lemma findn_fresh:
  assumes a: "x♯θ_n"
  shows "findn θ_n x = None"
  using a
  apply(induct θ_n)
   apply(auto simp add: fresh_list_cons fresh_atm fresh_prod)
  done

fun 
  findc :: "(coname×name×trm) list⇒coname⇒(name×trm) option"
  where
    "findc [] x = None"
  | "findc ((c,y,P)#θ_c) a = (if a=c then Some (y,P) else findc θ_c a)"

lemma findc_eqvt[eqvt]:
  fixes pi1::"name prm"
    and   pi2::"coname prm"
  shows "(pi1∙findc θ_c a) = findc (pi1∙θ_c) (pi1∙a)" 
    and   "(pi2∙findc θ_c a) = findc (pi2∙θ_c) (pi2∙a)"
   apply(induct θ_c)
     apply(auto simp add: perm_bij) 
  done

lemma findc_fresh:
  assumes a: "a♯θ_c"
  shows "findc θ_c a = None"
  using a
  apply(induct θ_c)
   apply(auto simp add: fresh_list_cons fresh_atm fresh_prod)
  done

abbreviation 
  nmaps :: "(name×coname×trm) list ⇒ name ⇒ (coname×trm) option ⇒ bool" (‹_ nmaps _ to _› [55,55,55] 55) 
  where
    "θ_n nmaps x to P ≡ (findn θ_n x) = P"

abbreviation 
  cmaps :: "(coname×name×trm) list ⇒ coname ⇒ (name×trm) option ⇒ bool" (‹_ cmaps _ to _› [55,55,55] 55) 
  where
    "θ_c cmaps a to P ≡ (findc θ_c a) = P"

lemma nmaps_fresh:
  shows "θ_n nmaps x to Some (c,P) ⟹ a♯θ_n ⟹ a♯(c,P)"
  apply(induct θ_n)
   apply(auto simp add: fresh_list_cons fresh_prod fresh_atm)
   apply(case_tac "aa=x")
    apply(auto)
  apply(case_tac "aa=x")
   apply(auto)
  done

lemma cmaps_fresh:
  shows "θ_c cmaps a to Some (y,P) ⟹ x♯θ_c ⟹ x♯(y,P)"
  apply(induct θ_c)
   apply(auto simp add: fresh_list_cons fresh_prod fresh_atm)
   apply(case_tac "a=aa")
    apply(auto)
  apply(case_tac "a=aa")
   apply(auto)
  done

lemma nmaps_false:
  shows "θ_n nmaps x to Some (c,P) ⟹ x♯θ_n ⟹ False"
  apply(induct θ_n)
   apply(auto simp add: fresh_list_cons fresh_prod fresh_atm)
  done

lemma cmaps_false:
  shows "θ_c cmaps c to Some (x,P) ⟹ c♯θ_c ⟹ False"
  apply(induct θ_c)
   apply(auto simp add: fresh_list_cons fresh_prod fresh_atm)
  done

fun 
  lookupa :: "name⇒coname⇒(coname×name×trm) list⇒trm"
  where
    "lookupa x a [] = Ax x a"
  | "lookupa x a ((c,y,P)#θ_c) = (if a=c then Cut <a>.Ax x a (y).P else lookupa x a θ_c)"

lemma lookupa_eqvt[eqvt]:
  fixes pi1::"name prm"
    and   pi2::"coname prm"
  shows "(pi1∙(lookupa x a θ_c)) = lookupa (pi1∙x) (pi1∙a) (pi1∙θ_c)"
    and   "(pi2∙(lookupa x a θ_c)) = lookupa (pi2∙x) (pi2∙a) (pi2∙θ_c)"
   apply -
   apply(induct θ_c)
    apply(auto simp add: eqvts)
  apply(induct θ_c)
   apply(auto simp add: eqvts)
  done

lemma lookupa_fire:
  assumes a: "θ_c cmaps a to Some (y,P)"
  shows "(lookupa x a θ_c) = Cut <a>.Ax x a (y).P"
  using a
  apply(induct θ_c arbitrary: x a y P)
   apply(auto)
  done

fun 
  lookupb :: "name⇒coname⇒(coname×name×trm) list⇒coname⇒trm⇒trm"
  where
    "lookupb x a [] c P = Cut <c>.P (x).Ax x a"
  | "lookupb x a ((d,y,N)#θ_c) c P = (if a=d then Cut <c>.P (y).N  else lookupb x a θ_c c P)"

lemma lookupb_eqvt[eqvt]:
  fixes pi1::"name prm"
    and   pi2::"coname prm"
  shows "(pi1∙(lookupb x a θ_c c P)) = lookupb (pi1∙x) (pi1∙a) (pi1∙θ_c) (pi1∙c) (pi1∙P)"
    and   "(pi2∙(lookupb x a θ_c c P)) = lookupb (pi2∙x) (pi2∙a) (pi2∙θ_c) (pi2∙c) (pi2∙P)"
   apply -
   apply(induct θ_c)
    apply(auto simp add: eqvts)
  apply(induct θ_c)
   apply(auto simp add: eqvts)
  done

fun 
  lookup :: "name⇒coname⇒(name×coname×trm) list⇒(coname×name×trm) list⇒trm"
  where
    "lookup x a [] θ_c = lookupa x a θ_c"
  | "lookup x a ((y,c,P)#θ_n) θ_c = (if x=y then (lookupb x a θ_c c P) else lookup x a θ_n θ_c)"

lemma lookup_eqvt[eqvt]:
  fixes pi1::"name prm"
    and   pi2::"coname prm"
  shows "(pi1∙(lookup x a θ_n θ_c)) = lookup (pi1∙x) (pi1∙a) (pi1∙θ_n) (pi1∙θ_c)"
    and   "(pi2∙(lookup x a θ_n θ_c)) = lookup (pi2∙x) (pi2∙a) (pi2∙θ_n) (pi2∙θ_c)"
   apply -
   apply(induct θ_n)
    apply(auto simp add: eqvts)
  apply(induct θ_n)
   apply(auto simp add: eqvts)
  done

fun 
  lookupc :: "name⇒coname⇒(name×coname×trm) list⇒trm"
  where
    "lookupc x a [] = Ax x a"
  | "lookupc x a ((y,c,P)#θ_n) = (if x=y then P[c⊢c>a] else lookupc x a θ_n)"

lemma lookupc_eqvt[eqvt]:
  fixes pi1::"name prm"
    and   pi2::"coname prm"
  shows "(pi1∙(lookupc x a θ_n)) = lookupc (pi1∙x) (pi1∙a) (pi1∙θ_n)"
    and   "(pi2∙(lookupc x a θ_n)) = lookupc (pi2∙x) (pi2∙a) (pi2∙θ_n)"
   apply -
   apply(induct θ_n)
    apply(auto simp add: eqvts)
  apply(induct θ_n)
   apply(auto simp add: eqvts)
  done

fun 
  lookupd :: "name⇒coname⇒(coname×name×trm) list⇒trm"
  where
    "lookupd x a [] = Ax x a"
  | "lookupd x a ((c,y,P)#θ_c) = (if a=c then P[y⊢n>x] else lookupd x a θ_c)"

lemma lookupd_eqvt[eqvt]:
  fixes pi1::"name prm"
    and   pi2::"coname prm"
  shows "(pi1∙(lookupd x a θ_n)) = lookupd (pi1∙x) (pi1∙a) (pi1∙θ_n)"
    and   "(pi2∙(lookupd x a θ_n)) = lookupd (pi2∙x) (pi2∙a) (pi2∙θ_n)"
   apply -
   apply(induct θ_n)
    apply(auto simp add: eqvts)
  apply(induct θ_n)
   apply(auto simp add: eqvts)
  done

lemma lookupa_fresh:
  assumes a: "a♯θ_c"
  shows "lookupa y a θ_c = Ax y a"
  using a
  apply(induct θ_c)
   apply(auto simp add: fresh_prod fresh_list_cons fresh_atm)
  done

lemma lookupa_csubst:
  assumes a: "a♯θ_c"
  shows "Cut <a>.Ax y a (x).P = (lookupa y a θ_c){a:=(x).P}"
  using a by (simp add: lookupa_fresh)

lemma lookupa_freshness:
  fixes a::"coname"
    and   x::"name"
  shows "a♯(θ_c,c) ⟹ a♯lookupa y c θ_c"
    and   "x♯(θ_c,y) ⟹ x♯lookupa y c θ_c"
   apply(induct θ_c)
     apply(auto simp add: fresh_prod fresh_list_cons abs_fresh fresh_atm)
  done

lemma lookupa_unicity:
  assumes a: "lookupa x a θ_c= Ax y b" "b♯θ_c" "y♯θ_c"
  shows "x=y ∧ a=b"
  using a
  apply(induct θ_c)
   apply(auto simp add: trm.inject fresh_list_cons fresh_prod fresh_atm)
   apply(case_tac "a=aa")
    apply(auto)
  apply(case_tac "a=aa")
   apply(auto)
  done

lemma lookupb_csubst:
  assumes a: "a♯(θ_c,c,N)"
  shows "Cut <c>.N (x).P = (lookupb y a θ_c c N){a:=(x).P}"
  using a
  apply(induct θ_c)
   apply(auto simp add: fresh_list_cons fresh_atm fresh_prod)
  apply(rule sym)
  apply(generate_fresh "name")
  apply(generate_fresh "coname")
  apply(subgoal_tac "Cut <c>.N (y).Ax y a = Cut <caa>.([(caa,c)]∙N) (ca).Ax ca a")
   apply(simp)
   apply(rule trans)
    apply(rule better_Cut_substc)
     apply(simp)
    apply(simp add: abs_fresh)
   apply(simp)
   apply(subgoal_tac "a♯([(caa,c)]∙N)")
    apply(simp add: forget)
    apply(simp add: trm.inject)
   apply(simp add: fresh_left calc_atm fresh_prod fresh_atm)
  apply(simp add: trm.inject)
  apply(rule conjI)
   apply(rule sym)
   apply(simp add: alpha fresh_prod fresh_atm)
  apply(simp add: alpha calc_atm fresh_prod fresh_atm)
  done

lemma lookupb_freshness:
  fixes a::"coname"
    and   x::"name"
  shows "a♯(θ_c,c,b,P) ⟹ a♯lookupb y c θ_c b P"
    and   "x♯(θ_c,y,P) ⟹ x♯lookupb y c θ_c b P"
   apply(induct θ_c)
     apply(auto simp add: fresh_prod fresh_list_cons abs_fresh fresh_atm)
  done

lemma lookupb_unicity:
  assumes a: "lookupb x a θ_c c P = Ax y b" "b♯(θ_c,c,P)" "y♯θ_c"
  shows "x=y ∧ a=b"
  using a
  apply(induct θ_c)
   apply(auto simp add: fresh_list_cons fresh_prod fresh_atm)
   apply(case_tac "a=aa")
    apply(auto)
  apply(case_tac "a=aa")
   apply(auto)
  done

lemma lookupb_lookupa:
  assumes a: "x♯θ_c"
  shows "lookupb x c θ_c a P = (lookupa x c θ_c){x:=<a>.P}"
  using a
  apply(induct θ_c)
   apply(auto simp add: fresh_list_cons fresh_prod)
  apply(generate_fresh "coname")
  apply(generate_fresh "name")
  apply(subgoal_tac "Cut <c>.Ax x c (aa).b = Cut <ca>.Ax x ca (caa).([(caa,aa)]∙b)")
   apply(simp)
   apply(rule sym)
   apply(rule trans)
    apply(rule better_Cut_substn)
     apply(simp add: abs_fresh)
    apply(simp)
   apply(simp)
   apply(subgoal_tac "x♯([(caa,aa)]∙b)")
    apply(simp add: forget)
    apply(simp add: trm.inject)
   apply(auto simp add: fresh_left calc_atm fresh_prod fresh_atm)[1]
  apply(simp add: trm.inject)
  apply(rule conjI)
   apply(simp add: alpha calc_atm fresh_atm fresh_prod)
  apply(rule sym)
  apply(simp add: alpha calc_atm fresh_atm fresh_prod)
  done

lemma lookup_csubst:
  assumes a: "a♯(θ_n,θ_c)"
  shows "lookup y c θ_n ((a,x,P)#θ_c) = (lookup y c θ_n θ_c){a:=(x).P}"
  using a
  apply(induct θ_n)
   apply(auto simp add: fresh_prod fresh_list_cons)
     apply(simp add: lookupa_csubst)
    apply(simp add: lookupa_freshness forget fresh_atm fresh_prod)
   apply(rule lookupb_csubst)
   apply(simp)
  apply(auto simp add: lookupb_freshness forget fresh_atm fresh_prod)
  done

lemma lookup_fresh:
  assumes a: "x♯(θ_n,θ_c)"
  shows "lookup x c θ_n θ_c = lookupa x c θ_c"
  using a
  apply(induct θ_n)
   apply(auto simp add: fresh_prod fresh_list_cons fresh_atm)
  done

lemma lookup_unicity:
  assumes a: "lookup x a θ_n θ_c= Ax y b" "b♯(θ_c,θ_n)" "y♯(θ_c,θ_n)"
  shows "x=y ∧ a=b"
  using a
  apply(induct θ_n)
   apply(auto simp add: trm.inject fresh_list_cons fresh_prod fresh_atm)
     apply(drule lookupa_unicity)
       apply(simp)+
    apply(drule lookupa_unicity)
      apply(simp)+
   apply(case_tac "x=aa")
    apply(auto)
   apply(drule lookupb_unicity)
     apply(simp add: fresh_atm)
    apply(simp)
   apply(simp)
  apply(case_tac "x=aa")
   apply(auto)
  apply(drule lookupb_unicity)
    apply(simp add: fresh_atm)
   apply(simp)
  apply(simp)
  done

lemma lookup_freshness:
  fixes a::"coname"
    and   x::"name"
  shows "a♯(c,θ_c,θ_n) ⟹ a♯lookup y c θ_n θ_c"
    and   "x♯(y,θ_c,θ_n) ⟹ x♯lookup y c θ_n θ_c"   
   apply(induct θ_n)
     apply(auto simp add: fresh_prod fresh_list_cons abs_fresh fresh_atm)
     apply(simp add: fresh_atm fresh_prod lookupa_freshness)
    apply(simp add: fresh_atm fresh_prod lookupa_freshness)
   apply(simp add: fresh_atm fresh_prod lookupb_freshness)
  apply(simp add: fresh_atm fresh_prod lookupb_freshness)
  done

lemma lookupc_freshness:
  fixes a::"coname"
    and   x::"name"
  shows "a♯(θ_c,c) ⟹ a♯lookupc y c θ_c"
    and   "x♯(θ_c,y) ⟹ x♯lookupc y c θ_c"
   apply(induct θ_c)
     apply(auto simp add: fresh_prod fresh_list_cons abs_fresh fresh_atm)
   apply(rule rename_fresh)
   apply(simp add: fresh_atm)
  apply(rule rename_fresh)
  apply(simp add: fresh_atm)
  done

lemma lookupc_fresh:
  assumes a: "y♯θ_n"
  shows "lookupc y a θ_n = Ax y a"
  using a
  apply(induct θ_n)
   apply(auto simp add: fresh_prod fresh_list_cons fresh_atm)
  done

lemma lookupc_nmaps:
  assumes a: "θ_n nmaps x to Some (c,P)"
  shows "lookupc x a θ_n = P[c⊢c>a]"
  using a
  apply(induct θ_n)
   apply(auto)
  done 

lemma lookupc_unicity:
  assumes a: "lookupc y a θ_n = Ax x b" "x♯θ_n"
  shows "y=x"
  using a
  apply(induct θ_n)
   apply(auto simp add: trm.inject fresh_list_cons fresh_prod)
  apply(case_tac "y=aa")
   apply(auto)
  apply(subgoal_tac "x♯(ba[aa⊢c>a])")
   apply(simp add: fresh_atm)
  apply(rule rename_fresh)
  apply(simp)
  done

lemma lookupd_fresh:
  assumes a: "a♯θ_c"
  shows "lookupd y a θ_c = Ax y a"
  using a
  apply(induct θ_c)
   apply(auto simp add: fresh_prod fresh_list_cons fresh_atm)
  done 

lemma lookupd_unicity:
  assumes a: "lookupd y a θ_c = Ax y b" "b♯θ_c"
  shows "a=b"
  using a
  apply(induct θ_c)
   apply(auto simp add: trm.inject fresh_list_cons fresh_prod)
  apply(case_tac "a=aa")
   apply(auto)
  apply(subgoal_tac "b♯(ba[aa⊢n>y])")
   apply(simp add: fresh_atm)
  apply(rule rename_fresh)
  apply(simp)
  done

lemma lookupd_freshness:
  fixes a::"coname"
    and   x::"name"
  shows "a♯(θ_c,c) ⟹ a♯lookupd y c θ_c"
    and   "x♯(θ_c,y) ⟹ x♯lookupd y c θ_c"
   apply(induct θ_c)
     apply(auto simp add: fresh_prod fresh_list_cons abs_fresh fresh_atm)
   apply(rule rename_fresh)
   apply(simp add: fresh_atm)
  apply(rule rename_fresh)
  apply(simp add: fresh_atm)
  done

lemma lookupd_cmaps:
  assumes a: "θ_c cmaps a to Some (x,P)"
  shows "lookupd y a θ_c = P[x⊢n>y]"
  using a
  apply(induct θ_c)
   apply(auto)
  done 

nominal_primrec (freshness_context: "θ_n::(name×coname×trm)")
  stn :: "trm⇒(name×coname×trm) list⇒trm" 
  where
    "stn (Ax x a) θ_n = lookupc x a θ_n"
  | "⟦a♯(N,θ_n);x♯(M,θ_n)⟧ ⟹ stn (Cut <a>.M (x).N) θ_n = (Cut <a>.M (x).N)" 
  | "x♯θ_n ⟹ stn (NotR (x).M a) θ_n = (NotR (x).M a)"
  | "a♯θ_n ⟹stn (NotL <a>.M x) θ_n = (NotL <a>.M x)"
  | "⟦a♯(N,d,b,θ_n);b♯(M,d,a,θ_n)⟧ ⟹ stn (AndR <a>.M <b>.N d) θ_n = (AndR <a>.M <b>.N d)"
  | "x♯(z,θ_n) ⟹ stn (AndL1 (x).M z) θ_n = (AndL1 (x).M z)"
  | "x♯(z,θ_n) ⟹ stn (AndL2 (x).M z) θ_n = (AndL2 (x).M z)"
  | "a♯(b,θ_n) ⟹ stn (OrR1 <a>.M b) θ_n = (OrR1 <a>.M b)"
  | "a♯(b,θ_n) ⟹ stn (OrR2 <a>.M b) θ_n = (OrR2 <a>.M b)"
  | "⟦x♯(N,z,u,θ_n);u♯(M,z,x,θ_n)⟧ ⟹ stn (OrL (x).M (u).N z) θ_n = (OrL (x).M (u).N z)"
  | "⟦a♯(b,θ_n);x♯θ_n⟧ ⟹ stn (ImpR (x).<a>.M b) θ_n = (ImpR (x).<a>.M b)"
  | "⟦a♯(N,θ_n);x♯(M,z,θ_n)⟧ ⟹ stn (ImpL <a>.M (x).N z) θ_n = (ImpL <a>.M (x).N z)"
                       apply(finite_guess)+
                       apply(rule TrueI)+
                       apply(simp add: abs_fresh abs_supp fin_supp)+
                       apply(fresh_guess)+
  done

nominal_primrec (freshness_context: "θ_c::(coname×name×trm)")
  stc :: "trm⇒(coname×name×trm) list⇒trm" 
  where
    "stc (Ax x a) θ_c = lookupd x a θ_c"
  | "⟦a♯(N,θ_c);x♯(M,θ_c)⟧ ⟹ stc (Cut <a>.M (x).N) θ_c = (Cut <a>.M (x).N)" 
  | "x♯θ_c ⟹ stc (NotR (x).M a) θ_c = (NotR (x).M a)"
  | "a♯θ_c ⟹ stc (NotL <a>.M x) θ_c = (NotL <a>.M x)"
  | "⟦a♯(N,d,b,θ_c);b♯(M,d,a,θ_c)⟧ ⟹ stc (AndR <a>.M <b>.N d) θ_c = (AndR <a>.M <b>.N d)"
  | "x♯(z,θ_c) ⟹ stc (AndL1 (x).M z) θ_c = (AndL1 (x).M z)"
  | "x♯(z,θ_c) ⟹ stc (AndL2 (x).M z) θ_c = (AndL2 (x).M z)"
  | "a♯(b,θ_c) ⟹ stc (OrR1 <a>.M b) θ_c = (OrR1 <a>.M b)"
  | "a♯(b,θ_c) ⟹ stc (OrR2 <a>.M b) θ_c = (OrR2 <a>.M b)"
  | "⟦x♯(N,z,u,θ_c);u♯(M,z,x,θ_c)⟧ ⟹ stc (OrL (x).M (u).N z) θ_c = (OrL (x).M (u).N z)"
  | "⟦a♯(b,θ_c);x♯θ_c⟧ ⟹ stc (ImpR (x).<a>.M b) θ_c = (ImpR (x).<a>.M b)"
  | "⟦a♯(N,θ_c);x♯(M,z,θ_c)⟧ ⟹ stc (ImpL <a>.M (x).N z) θ_c = (ImpL <a>.M (x).N z)"
                       apply(finite_guess)+
                       apply(rule TrueI)+
                       apply(simp add: abs_fresh abs_supp fin_supp)+
                       apply(fresh_guess)+
  done

lemma stn_eqvt[eqvt]:
  fixes pi1::"name prm"
    and   pi2::"coname prm"
  shows "(pi1∙(stn M θ_n)) = stn (pi1∙M) (pi1∙θ_n)"
    and   "(pi2∙(stn M θ_n)) = stn (pi2∙M) (pi2∙θ_n)"
   apply -
   apply(nominal_induct M avoiding: θ_n rule: trm.strong_induct)
              apply(auto simp add: eqvts fresh_bij fresh_prod eq_bij fresh_atm)
  apply(nominal_induct M avoiding: θ_n rule: trm.strong_induct)
             apply(auto simp add: eqvts fresh_bij fresh_prod eq_bij fresh_atm)
  done

lemma stc_eqvt[eqvt]:
  fixes pi1::"name prm"
    and   pi2::"coname prm"
  shows "(pi1∙(stc M θ_c)) = stc (pi1∙M) (pi1∙θ_c)"
    and   "(pi2∙(stc M θ_c)) = stc (pi2∙M) (pi2∙θ_c)"
   apply -
   apply(nominal_induct M avoiding: θ_c rule: trm.strong_induct)
              apply(auto simp add: eqvts fresh_bij fresh_prod eq_bij fresh_atm)
  apply(nominal_induct M avoiding: θ_c rule: trm.strong_induct)
             apply(auto simp add: eqvts fresh_bij fresh_prod eq_bij fresh_atm)
  done

lemma stn_fresh:
  fixes a::"coname"
    and   x::"name"
  shows "a♯(θ_n,M) ⟹ a♯stn M θ_n"
    and   "x♯(θ_n,M) ⟹ x♯stn M θ_n"
   apply(nominal_induct M avoiding: θ_n a x rule: trm.strong_induct)
                       apply(auto simp add: abs_fresh fresh_prod fresh_atm)
   apply(rule lookupc_freshness)
   apply(simp add: fresh_atm)
  apply(rule lookupc_freshness)
  apply(simp add: fresh_atm)
  done

lemma stc_fresh:
  fixes a::"coname"
    and   x::"name"
  shows "a♯(θ_c,M) ⟹ a♯stc M θ_c"
    and   "x♯(θ_c,M) ⟹ x♯stc M θ_c"
   apply(nominal_induct M avoiding: θ_c a x rule: trm.strong_induct)
                       apply(auto simp add: abs_fresh fresh_prod fresh_atm)
   apply(rule lookupd_freshness)
   apply(simp add: fresh_atm)
  apply(rule lookupd_freshness)
  apply(simp add: fresh_atm)
  done

lemma case_option_eqvt1[eqvt_force]:
  fixes pi1::"name prm"
    and   pi2::"coname prm"
    and   B::"(name×trm) option"
    and   r::"trm"
  shows "(pi1∙(case B of Some (x,P) ⇒ s x P | None ⇒ r)) = 
              (case (pi1∙B) of Some (x,P) ⇒ (pi1∙s) x P | None ⇒ (pi1∙r))"
    and   "(pi2∙(case B of Some (x,P) ⇒ s x P| None ⇒ r)) = 
              (case (pi2∙B) of Some (x,P) ⇒ (pi2∙s) x P | None ⇒ (pi2∙r))"
   apply(cases "B")
    apply(auto)
   apply(perm_simp)
  apply(cases "B")
   apply(auto)
  apply(perm_simp)
  done

lemma case_option_eqvt2[eqvt_force]:
  fixes pi1::"name prm"
    and   pi2::"coname prm"
    and   B::"(coname×trm) option"
    and   r::"trm"
  shows "(pi1∙(case B of Some (x,P) ⇒ s x P | None ⇒ r)) = 
              (case (pi1∙B) of Some (x,P) ⇒ (pi1∙s) x P | None ⇒ (pi1∙r))"
    and   "(pi2∙(case B of Some (x,P) ⇒ s x P| None ⇒ r)) = 
              (case (pi2∙B) of Some (x,P) ⇒ (pi2∙s) x P | None ⇒ (pi2∙r))"
   apply(cases "B")
    apply(auto)
   apply(perm_simp)
  apply(cases "B")
   apply(auto)
  apply(perm_simp)
  done

nominal_primrec (freshness_context: "(θ_n::(name×coname×trm) list,θ_c::(coname×name×trm) list)")
  psubst :: "(name×coname×trm) list⇒(coname×name×trm) list⇒trm⇒trm" (‹_,_<_>› [100,100,100] 100) 
  where
    "θ_n,θ_c<Ax x a> = lookup x a θ_n θ_c" 
  | "⟦a♯(N,θ_n,θ_c);x♯(M,θ_n,θ_c)⟧ ⟹ θ_n,θ_c<Cut <a>.M (x).N> = 
   Cut <a>.(if ∃x. M=Ax x a then stn M θ_n else θ_n,θ_c<M>) 
       (x).(if ∃a. N=Ax x a then stc N θ_c else θ_n,θ_c<N>)" 
  | "x♯(θ_n,θ_c) ⟹ θ_n,θ_c<NotR (x).M a> = 
  (case (findc θ_c a) of 
       Some (u,P) ⇒ fresh_fun (λa'. Cut <a'>.NotR (x).(θ_n,θ_c<M>) a' (u).P) 
     | None ⇒ NotR (x).(θ_n,θ_c<M>) a)"
  | "a♯(θ_n,θ_c) ⟹ θ_n,θ_c<NotL <a>.M x> = 
  (case (findn θ_n x) of 
       Some (c,P) ⇒ fresh_fun (λx'. Cut <c>.P (x').(NotL <a>.(θ_n,θ_c<M>) x')) 
     | None ⇒ NotL <a>.(θ_n,θ_c<M>) x)"
  | "⟦a♯(N,c,θ_n,θ_c);b♯(M,c,θ_n,θ_c);b≠a⟧ ⟹ (θ_n,θ_c<AndR <a>.M <b>.N c>) = 
  (case (findc θ_c c) of 
       Some (x,P) ⇒ fresh_fun (λa'. Cut <a'>.(AndR <a>.(θ_n,θ_c<M>) <b>.(θ_n,θ_c<N>) a') (x).P)
     | None ⇒ AndR <a>.(θ_n,θ_c<M>) <b>.(θ_n,θ_c<N>) c)"
  | "x♯(z,θ_n,θ_c) ⟹ (θ_n,θ_c<AndL1 (x).M z>) = 
  (case (findn θ_n z) of 
       Some (c,P) ⇒ fresh_fun (λz'. Cut <c>.P (z').AndL1 (x).(θ_n,θ_c<M>) z') 
     | None ⇒ AndL1 (x).(θ_n,θ_c<M>) z)"
  | "x♯(z,θ_n,θ_c) ⟹ (θ_n,θ_c<AndL2 (x).M z>) = 
  (case (findn θ_n z) of 
       Some (c,P) ⇒ fresh_fun (λz'. Cut <c>.P (z').AndL2 (x).(θ_n,θ_c<M>) z') 
     | None ⇒ AndL2 (x).(θ_n,θ_c<M>) z)"
  | "⟦x♯(N,z,θ_n,θ_c);u♯(M,z,θ_n,θ_c);x≠u⟧ ⟹ (θ_n,θ_c<OrL (x).M (u).N z>) =
  (case (findn θ_n z) of  
       Some (c,P) ⇒ fresh_fun (λz'. Cut <c>.P (z').OrL (x).(θ_n,θ_c<M>) (u).(θ_n,θ_c<N>) z') 
     | None ⇒ OrL (x).(θ_n,θ_c<M>) (u).(θ_n,θ_c<N>) z)"
  | "a♯(b,θ_n,θ_c) ⟹ (θ_n,θ_c<OrR1 <a>.M b>) = 
  (case (findc θ_c b) of
       Some (x,P) ⇒ fresh_fun (λa'. Cut <a'>.OrR1 <a>.(θ_n,θ_c<M>) a' (x).P) 
     | None ⇒ OrR1 <a>.(θ_n,θ_c<M>) b)"
  | "a♯(b,θ_n,θ_c) ⟹ (θ_n,θ_c<OrR2 <a>.M b>) = 
  (case (findc θ_c b) of
       Some (x,P) ⇒ fresh_fun (λa'. Cut <a'>.OrR2 <a>.(θ_n,θ_c<M>) a' (x).P) 
     | None ⇒ OrR2 <a>.(θ_n,θ_c<M>) b)"
  | "⟦a♯(b,θ_n,θ_c); x♯(θ_n,θ_c)⟧ ⟹ (θ_n,θ_c<ImpR (x).<a>.M b>) = 
  (case (findc θ_c b) of
       Some (z,P) ⇒ fresh_fun (λa'. Cut <a'>.ImpR (x).<a>.(θ_n,θ_c<M>) a' (z).P)
     | None ⇒ ImpR (x).<a>.(θ_n,θ_c<M>) b)"
  | "⟦a♯(N,θ_n,θ_c); x♯(z,M,θ_n,θ_c)⟧ ⟹ (θ_n,θ_c<ImpL <a>.M (x).N z>) = 
  (case (findn θ_n z) of
       Some (c,P) ⇒ fresh_fun (λz'. Cut <c>.P (z').ImpL <a>.(θ_n,θ_c<M>) (x).(θ_n,θ_c<N>) z') 
     | None ⇒ ImpL <a>.(θ_n,θ_c<M>) (x).(θ_n,θ_c<N>) z)"
                       apply(finite_guess)+
                       apply(rule TrueI)+
                       apply(simp add: abs_fresh stc_fresh)
                       apply(simp add: abs_fresh stn_fresh)
                       apply(case_tac "findc θ_c x3")
                       apply(simp add: abs_fresh)
                       apply(auto)[1]
                       apply(generate_fresh "coname")
                       apply(fresh_fun_simp (no_asm))
                       apply(drule cmaps_fresh)
                       apply(auto simp add: fresh_prod)[1]
                       apply(simp add: abs_fresh fresh_prod fresh_atm)
                       apply(case_tac "findn θ_n x3")
                       apply(simp add: abs_fresh)
                       apply(auto)[1]
                       apply(generate_fresh "name")
                       apply(fresh_fun_simp (no_asm))
                       apply(drule nmaps_fresh)
                       apply(auto simp add: fresh_prod)[1]
                       apply(simp add: abs_fresh fresh_prod fresh_atm)
                       apply(case_tac "findc θ_c x5")
                       apply(simp add: abs_fresh)
                       apply(auto)[1]
                       apply(generate_fresh "coname")
                       apply(fresh_fun_simp (no_asm))
                       apply(drule cmaps_fresh)
                       apply(auto simp add: fresh_prod)[1]
                       apply(simp add: abs_fresh fresh_prod fresh_atm)
                       apply(case_tac "findc θ_c x5")
                       apply(simp add: abs_fresh)
                       apply(auto)[1]
                       apply(generate_fresh "coname")
                       apply(fresh_fun_simp (no_asm))
                       apply(drule_tac x="x3" in cmaps_fresh)
                       apply(auto simp add: fresh_prod)[1]
                       apply(simp add: abs_fresh fresh_prod fresh_atm)
                       apply(case_tac "findn θ_n x3")
                       apply(simp add: abs_fresh)
                       apply(auto)[1]
                       apply(generate_fresh "name")
                       apply(fresh_fun_simp (no_asm))
                       apply(drule nmaps_fresh)
                       apply(auto simp add: fresh_prod)[1]
                       apply(simp add: abs_fresh fresh_prod fresh_atm)
                       apply(case_tac "findn θ_n x3")
                       apply(simp add: abs_fresh)
                       apply(auto)[1]
                       apply(generate_fresh "name")
                       apply(fresh_fun_simp (no_asm))
                       apply(drule nmaps_fresh)
                       apply(auto simp add: fresh_prod)[1]
                       apply(simp add: abs_fresh fresh_prod fresh_atm)
                       apply(case_tac "findc θ_c x3")
                       apply(simp add: abs_fresh)
                       apply(auto)[1]
                       apply(generate_fresh "coname")
                       apply(fresh_fun_simp (no_asm))
                       apply(drule cmaps_fresh)
                       apply(auto simp add: fresh_prod)[1]
                       apply(simp add: abs_fresh fresh_prod fresh_atm)
                       apply(case_tac "findc θ_c x3")
                       apply(simp add: abs_fresh)
                       apply(auto)[1]
                       apply(generate_fresh "coname")
                       apply(fresh_fun_simp (no_asm))
                       apply(drule cmaps_fresh)
                       apply(auto simp add: fresh_prod)[1]
                       apply(simp add: abs_fresh fresh_prod fresh_atm)
                       apply(case_tac "findn θ_n x5")
                       apply(simp add: abs_fresh)
                       apply(auto)[1]
                       apply(generate_fresh "name")
                       apply(fresh_fun_simp (no_asm))
                       apply(drule nmaps_fresh)
                       apply(auto simp add: fresh_prod)[1]
                       apply(simp add: abs_fresh fresh_prod fresh_atm)
                       apply(case_tac "findn θ_n x5")
                       apply(simp add: abs_fresh)
                       apply(auto)[1]
                       apply(generate_fresh "name")
                       apply(fresh_fun_simp (no_asm))
                       apply(drule_tac a="x3" in nmaps_fresh)
                       apply(auto simp add: fresh_prod)[1]
                       apply(simp add: abs_fresh fresh_prod fresh_atm)
                       apply(case_tac "findc θ_c x4")
                       apply(simp add: abs_fresh abs_supp fin_supp)
                       apply(auto)[1]
                       apply(generate_fresh "coname")
                       apply(fresh_fun_simp (no_asm))
                       apply(drule cmaps_fresh)
                       apply(auto simp add: fresh_prod)[1]
                       apply(simp add: abs_fresh fresh_prod fresh_atm abs_supp fin_supp)
                       apply(case_tac "findc θ_c x4")
                       apply(simp add: abs_fresh abs_supp fin_supp)
                       apply(auto)[1]
                       apply(generate_fresh "coname")
                       apply(fresh_fun_simp (no_asm))
                       apply(drule_tac x="x2" in cmaps_fresh)
                       apply(auto simp add: fresh_prod)[1]
                       apply(simp add: abs_fresh fresh_prod fresh_atm abs_supp fin_supp)
                       apply(case_tac "findn θ_n x5")
                       apply(simp add: abs_fresh)
                       apply(auto)[1]
                       apply(generate_fresh "name")
                       apply(fresh_fun_simp (no_asm))
                       apply(drule nmaps_fresh)
                       apply(auto simp add: fresh_prod)[1]
                       apply(simp add: abs_fresh fresh_prod fresh_atm)
                       apply(case_tac "findn θ_n x5")
                       apply(simp add: abs_fresh)
                       apply(auto)[1]
                       apply(generate_fresh "name")
                       apply(fresh_fun_simp (no_asm))
                       apply(drule_tac a="x3" in nmaps_fresh)
                       apply(auto simp add: fresh_prod)[1]
                       apply(simp add: abs_fresh fresh_prod fresh_atm)
                       apply(fresh_guess)+
  done

lemma case_cong:
  assumes a: "B1=B2" "x1=x2" "y1=y2"
  shows "(case B1 of None ⇒ x1 | Some (x,P) ⇒ y1 x P) = (case B2 of None ⇒ x2 | Some (x,P) ⇒ y2 x P)"
  using a
  apply(auto)
  done

lemma find_maps:
  shows "θ_c cmaps a to (findc θ_c a)"
    and   "θ_n nmaps x to (findn θ_n x)"
   apply(auto)
  done

lemma psubst_eqvt[eqvt]:
  fixes pi1::"name prm"
    and   pi2::"coname prm"
  shows "pi1∙(θ_n,θ_c<M>) = (pi1∙θ_n),(pi1∙θ_c)<(pi1∙M)>"
    and   "pi2∙(θ_n,θ_c<M>) = (pi2∙θ_n),(pi2∙θ_c)<(pi2∙M)>"
   apply(nominal_induct M avoiding: θ_n θ_c rule: trm.strong_induct)
                       apply(auto simp add: eq_bij fresh_bij eqvts perm_pi_simp)
                     apply(rule case_cong)
                       apply(rule find_maps)
                      apply(simp)
                     apply(perm_simp add: eqvts)
                    apply(rule case_cong)
                      apply(rule find_maps)
                     apply(simp)
                    apply(perm_simp add: eqvts)
                   apply(rule case_cong)
                     apply(rule find_maps)
                    apply(simp)
                   apply(perm_simp add: eqvts)
                  apply(rule case_cong)
                    apply(rule find_maps)
                   apply(simp)
                  apply(perm_simp add: eqvts)
                 apply(rule case_cong)
                   apply(rule find_maps)
                  apply(simp)
                 apply(perm_simp add: eqvts)
                apply(rule case_cong)
                  apply(rule find_maps)
                 apply(simp)
                apply(perm_simp add: eqvts)
               apply(rule case_cong)
                 apply(rule find_maps)
                apply(simp)
               apply(perm_simp add: eqvts)
              apply(rule case_cong)
                apply(rule find_maps)
               apply(simp)
              apply(perm_simp add: eqvts)
             apply(rule case_cong)
               apply(rule find_maps)
              apply(simp)
             apply(perm_simp add: eqvts)
            apply(rule case_cong)
              apply(rule find_maps)
             apply(simp)
            apply(perm_simp add: eqvts)
           apply(rule case_cong)
             apply(rule find_maps)
            apply(simp)
           apply(perm_simp add: eqvts)
          apply(rule case_cong)
            apply(rule find_maps)
           apply(simp)
          apply(perm_simp add: eqvts)
         apply(rule case_cong)
           apply(rule find_maps)
          apply(simp)
         apply(perm_simp add: eqvts)
        apply(rule case_cong)
          apply(rule find_maps)
         apply(simp)
        apply(perm_simp add: eqvts)
       apply(rule case_cong)
         apply(rule find_maps)
        apply(simp)
       apply(perm_simp add: eqvts)
      apply(rule case_cong)
        apply(rule find_maps)
       apply(simp)
      apply(perm_simp add: eqvts)
     apply(rule case_cong)
       apply(rule find_maps)
      apply(simp)
     apply(perm_simp add: eqvts)
    apply(rule case_cong)
      apply(rule find_maps)
     apply(simp)
    apply(perm_simp add: eqvts)
   apply(rule case_cong)
     apply(rule find_maps)
    apply(simp)
   apply(perm_simp add: eqvts)
  apply(rule case_cong)
    apply(rule find_maps)
   apply(simp)
  apply(perm_simp add: eqvts)
  done

lemma ax_psubst:
  assumes a: "θ_n,θ_c<M> = Ax x a"
    and     b: "a♯(θ_n,θ_c)" "x♯(θ_n,θ_c)"
  shows "M = Ax x a"
  using a b
  apply(nominal_induct M avoiding: θ_n θ_c rule: trm.strong_induct)
             apply(auto)
            apply(drule lookup_unicity)
              apply(simp)+
           apply(case_tac "findc θ_c coname")
            apply(simp)
           apply(auto)[1]
           apply(generate_fresh "coname")
           apply(fresh_fun_simp)
           apply(simp)
          apply(case_tac "findn θ_n name")
           apply(simp)
          apply(auto)[1]
          apply(generate_fresh "name")
          apply(fresh_fun_simp)
          apply(simp)
         apply(case_tac "findc θ_c coname3")
          apply(simp)
         apply(auto)[1]
         apply(generate_fresh "coname")
         apply(fresh_fun_simp)
         apply(simp)
        apply(case_tac "findn θ_n name2")
         apply(simp)
        apply(auto)[1]
        apply(generate_fresh "name")
        apply(fresh_fun_simp)
        apply(simp)
       apply(case_tac "findn θ_n name2")
        apply(simp)
       apply(auto)[1]
       apply(generate_fresh "name")
       apply(fresh_fun_simp)
       apply(simp)
      apply(case_tac "findc θ_c coname2")
       apply(simp)
      apply(auto)[1]
      apply(generate_fresh "coname")
      apply(fresh_fun_simp)
      apply(simp)
     apply(case_tac "findc θ_c coname2")
      apply(simp)
     apply(auto)[1]
     apply(generate_fresh "coname")
     apply(fresh_fun_simp)
     apply(simp)
    apply(case_tac "findn θ_n name3")
     apply(simp)
    apply(auto)[1]
    apply(generate_fresh "name")
    apply(fresh_fun_simp)
    apply(simp)
   apply(case_tac "findc θ_c coname2")
    apply(simp)
   apply(auto)[1]
   apply(generate_fresh "coname")
   apply(fresh_fun_simp)
   apply(simp)
  apply(case_tac "findn θ_n name2")
   apply(simp)
  apply(auto)[1]
  apply(generate_fresh "name")
  apply(fresh_fun_simp)
  apply(simp)
  done

lemma better_Cut_substc1:
  assumes a: "a♯(P,b)" "b♯N" 
  shows "(Cut <a>.M (x).N){b:=(y).P} = Cut <a>.(M{b:=(y).P}) (x).N"
  using a
  apply -
  apply(generate_fresh "coname")
  apply(generate_fresh "name")
  apply(subgoal_tac "Cut <a>.M (x).N = Cut <c>.([(c,a)]∙M) (ca).([(ca,x)]∙N)")
   apply(simp)
   apply(rule trans)
    apply(rule better_Cut_substc)
     apply(simp)
    apply(simp add: abs_fresh)
   apply(auto)[1]
    apply(drule pt_bij1[OF pt_name_inst, OF at_name_inst])
    apply(simp add: calc_atm fresh_atm)
   apply(subgoal_tac"b♯([(ca,x)]∙N)")
    apply(simp add: forget)
    apply(simp add: trm.inject)
    apply(simp add: alpha eqvts calc_atm fresh_prod fresh_atm subst_fresh)[1]
    apply(perm_simp)
   apply(simp add: fresh_left calc_atm)
  apply(simp add: trm.inject)
  apply(rule conjI)
   apply(rule sym)
   apply(simp add: alpha eqvts calc_atm fresh_prod fresh_atm subst_fresh)[1]
  apply(rule sym)
  apply(simp add: alpha eqvts calc_atm fresh_prod fresh_atm subst_fresh)[1]
  done

lemma better_Cut_substc2:
  assumes a: "x♯(y,P)" "b♯(a,M)" "N≠Ax x b"
  shows "(Cut <a>.M (x).N){b:=(y).P} = Cut <a>.M (x).(N{b:=(y).P})"
  using a
  apply -
  apply(generate_fresh "coname")
  apply(generate_fresh "name")
  apply(subgoal_tac "Cut <a>.M (x).N = Cut <c>.([(c,a)]∙M) (ca).([(ca,x)]∙N)")
   apply(simp)
   apply(rule trans)
    apply(rule better_Cut_substc)
     apply(simp)
    apply(simp add: abs_fresh)
   apply(auto)[1]
    apply(drule pt_bij1[OF pt_name_inst, OF at_name_inst])
    apply(simp add: calc_atm fresh_atm fresh_prod)
   apply(subgoal_tac"b♯([(c,a)]∙M)")
    apply(simp add: forget)
    apply(simp add: trm.inject)
    apply(simp add: alpha eqvts calc_atm fresh_prod fresh_atm subst_fresh)[1]
    apply(perm_simp)
   apply(auto simp add: fresh_left calc_atm fresh_prod fresh_atm)[1]
  apply(simp add: trm.inject)
  apply(rule conjI)
   apply(rule sym)
   apply(simp add: alpha eqvts calc_atm fresh_prod fresh_atm subst_fresh)[1]
  apply(rule sym)
  apply(simp add: alpha eqvts calc_atm fresh_prod fresh_atm subst_fresh)[1]
  done

lemma better_Cut_substn1:
  assumes a: "y♯(x,N)" "a♯(b,P)" "M≠Ax y a"
  shows "(Cut <a>.M (x).N){y:=<b>.P} = Cut <a>.(M{y:=<b>.P}) (x).N"
  using a
  apply -
  apply(generate_fresh "coname")
  apply(generate_fresh "name")
  apply(subgoal_tac "Cut <a>.M (x).N = Cut <c>.([(c,a)]∙M) (ca).([(ca,x)]∙N)")
   apply(simp)
   apply(rule trans)
    apply(rule better_Cut_substn)
     apply(simp add: abs_fresh)
    apply(simp add: abs_fresh)
   apply(auto)[1]
    apply(drule pt_bij1[OF pt_coname_inst, OF at_coname_inst])
    apply(simp add: calc_atm fresh_atm fresh_prod)
   apply(subgoal_tac"y♯([(ca,x)]∙N)")
    apply(simp add: forget)
    apply(simp add: trm.inject)
    apply(simp add: alpha eqvts calc_atm fresh_prod fresh_atm subst_fresh)[1]
    apply(perm_simp)
   apply(auto simp add: fresh_left calc_atm fresh_prod fresh_atm)[1]
  apply(simp add: trm.inject)
  apply(rule conjI)
   apply(rule sym)
   apply(simp add: alpha eqvts calc_atm fresh_prod fresh_atm subst_fresh)[1]
  apply(rule sym)
  apply(simp add: alpha eqvts calc_atm fresh_prod fresh_atm subst_fresh)[1]
  done

lemma better_Cut_substn2:
  assumes a: "x♯(P,y)" "y♯M" 
  shows "(Cut <a>.M (x).N){y:=<b>.P} = Cut <a>.M (x).(N{y:=<b>.P})"
  using a
  apply -
  apply(generate_fresh "coname")
  apply(generate_fresh "name")
  apply(subgoal_tac "Cut <a>.M (x).N = Cut <c>.([(c,a)]∙M) (ca).([(ca,x)]∙N)")
   apply(simp)
   apply(rule trans)
    apply(rule better_Cut_substn)
     apply(simp add: abs_fresh)
    apply(simp add: abs_fresh)
   apply(auto)[1]
    apply(drule pt_bij1[OF pt_coname_inst, OF at_coname_inst])
    apply(simp add: calc_atm fresh_atm)
   apply(subgoal_tac"y♯([(c,a)]∙M)")
    apply(simp add: forget)
    apply(simp add: trm.inject)
    apply(simp add: alpha eqvts calc_atm fresh_prod fresh_atm subst_fresh)[1]
    apply(perm_simp)
   apply(simp add: fresh_left calc_atm)
  apply(simp add: trm.inject)
  apply(rule conjI)
   apply(rule sym)
   apply(simp add: alpha eqvts calc_atm fresh_prod fresh_atm subst_fresh)[1]
  apply(rule sym)
  apply(simp add: alpha eqvts calc_atm fresh_prod fresh_atm subst_fresh)[1]
  done

lemma psubst_fresh_name:
  fixes x::"name"
  assumes a: "x♯θ_n" "x♯θ_c" "x♯M"
  shows "x♯θ_n,θ_c<M>"
  using a
  apply(nominal_induct M avoiding: x θ_n θ_c rule: trm.strong_induct)
             apply(simp add: lookup_freshness)
            apply(auto simp add: abs_fresh)[1]
                 apply(simp add: lookupc_freshness)
                apply(simp add: lookupc_freshness)
               apply(simp add: lookupc_freshness)
              apply(simp add: lookupd_freshness)
             apply(simp add: lookupd_freshness)
            apply(simp add: lookupc_freshness)
           apply(simp)
           apply(case_tac "findc θ_c coname")
            apply(auto simp add: abs_fresh)[1]
           apply(auto)[1]
           apply(generate_fresh "coname")
           apply(fresh_fun_simp)
           apply(simp add: abs_fresh fresh_prod fresh_atm cmaps_fresh)
          apply(simp)
          apply(case_tac "findn θ_n name")
           apply(auto simp add: abs_fresh)[1]
          apply(auto)[1]
          apply(generate_fresh "name")
          apply(fresh_fun_simp)
          apply(simp add: abs_fresh fresh_prod fresh_atm nmaps_fresh)
         apply(simp)
         apply(case_tac "findc θ_c coname3")
          apply(auto simp add: abs_fresh)[1]
         apply(auto)[1]
         apply(generate_fresh "coname")
         apply(fresh_fun_simp)
         apply(simp add: abs_fresh fresh_prod fresh_atm cmaps_fresh)
        apply(simp)
        apply(case_tac "findn θ_n name2")
         apply(auto simp add: abs_fresh)[1]
        apply(auto)[1]
        apply(generate_fresh "name")
        apply(fresh_fun_simp)
        apply(simp add: abs_fresh fresh_prod fresh_atm nmaps_fresh)
       apply(simp)
       apply(case_tac "findn θ_n name2")
        apply(auto simp add: abs_fresh)[1]
       apply(auto)[1]
       apply(generate_fresh "name")
       apply(fresh_fun_simp)
       apply(simp add: abs_fresh fresh_prod fresh_atm nmaps_fresh)
      apply(simp)
      apply(case_tac "findc θ_c coname2")
       apply(auto simp add: abs_fresh)[1]
      apply(auto)[1]
      apply(generate_fresh "coname")
      apply(fresh_fun_simp)
      apply(simp add: abs_fresh fresh_prod fresh_atm cmaps_fresh)
     apply(simp)
     apply(case_tac "findc θ_c coname2")
      apply(auto simp add: abs_fresh)[1]
     apply(auto)[1]
     apply(generate_fresh "coname")
     apply(fresh_fun_simp)
     apply(simp add: abs_fresh fresh_prod fresh_atm cmaps_fresh)
    apply(simp)
    apply(case_tac "findn θ_n name3")
     apply(auto simp add: abs_fresh)[1]
    apply(auto)[1]
    apply(generate_fresh "name")
    apply(fresh_fun_simp)
    apply(simp add: abs_fresh fresh_prod fresh_atm nmaps_fresh)
   apply(simp)
   apply(case_tac "findc θ_c coname2")
    apply(auto simp add: abs_fresh abs_supp fin_supp)[1]
   apply(auto)[1]
   apply(generate_fresh "coname")
   apply(fresh_fun_simp)
   apply(simp add: abs_fresh abs_supp fin_supp fresh_prod fresh_atm cmaps_fresh)
  apply(simp)
  apply(case_tac "findn θ_n name2")
   apply(auto simp add: abs_fresh)[1]
  apply(auto)[1]
  apply(generate_fresh "name")
  apply(fresh_fun_simp)
  apply(simp add: abs_fresh fresh_prod fresh_atm nmaps_fresh)
  done

lemma psubst_fresh_coname:
  fixes a::"coname"
  assumes a: "a♯θ_n" "a♯θ_c" "a♯M"
  shows "a♯θ_n,θ_c<M>"
  using a
  apply(nominal_induct M avoiding: a θ_n θ_c rule: trm.strong_induct)
             apply(simp add: lookup_freshness)
            apply(auto simp add: abs_fresh)[1]
                 apply(simp add: lookupd_freshness)
                apply(simp add: lookupd_freshness)
               apply(simp add: lookupc_freshness)
              apply(simp add: lookupd_freshness)
             apply(simp add: lookupc_freshness)
            apply(simp add: lookupd_freshness)
           apply(simp)
           apply(case_tac "findc θ_c coname")
            apply(auto simp add: abs_fresh)[1]
           apply(auto)[1]
           apply(generate_fresh "coname")
           apply(fresh_fun_simp)
           apply(simp add: abs_fresh fresh_prod fresh_atm cmaps_fresh)
          apply(simp)
          apply(case_tac "findn θ_n name")
           apply(auto simp add: abs_fresh)[1]
          apply(auto)[1]
          apply(generate_fresh "name")
          apply(fresh_fun_simp)
          apply(simp add: abs_fresh fresh_prod fresh_atm nmaps_fresh)
         apply(simp)
         apply(case_tac "findc θ_c coname3")
          apply(auto simp add: abs_fresh)[1]
         apply(auto)[1]
         apply(generate_fresh "coname")
         apply(fresh_fun_simp)
         apply(simp add: abs_fresh fresh_prod fresh_atm cmaps_fresh)
        apply(simp)
        apply(case_tac "findn θ_n name2")
         apply(auto simp add: abs_fresh)[1]
        apply(auto)[1]
        apply(generate_fresh "name")
        apply(fresh_fun_simp)
        apply(simp add: abs_fresh fresh_prod fresh_atm nmaps_fresh)
       apply(simp)
       apply(case_tac "findn θ_n name2")
        apply(auto simp add: abs_fresh)[1]
       apply(auto)[1]
       apply(generate_fresh "name")
       apply(fresh_fun_simp)
       apply(simp add: abs_fresh fresh_prod fresh_atm nmaps_fresh)
      apply(simp)
      apply(case_tac "findc θ_c coname2")
       apply(auto simp add: abs_fresh)[1]
      apply(auto)[1]
      apply(generate_fresh "coname")
      apply(fresh_fun_simp)
      apply(simp add: abs_fresh fresh_prod fresh_atm cmaps_fresh)
     apply(simp)
     apply(case_tac "findc θ_c coname2")
      apply(auto simp add: abs_fresh)[1]
     apply(auto)[1]
     apply(generate_fresh "coname")
     apply(fresh_fun_simp)
     apply(simp add: abs_fresh fresh_prod fresh_atm cmaps_fresh)
    apply(simp)
    apply(case_tac "findn θ_n name3")
     apply(auto simp add: abs_fresh)[1]
    apply(auto)[1]
    apply(generate_fresh "name")
    apply(fresh_fun_simp)
    apply(simp add: abs_fresh fresh_prod fresh_atm nmaps_fresh)
   apply(simp)
   apply(case_tac "findc θ_c coname2")
    apply(auto simp add: abs_fresh abs_supp fin_supp)[1]
   apply(auto)[1]
   apply(generate_fresh "coname")
   apply(fresh_fun_simp)
   apply(simp add: abs_fresh abs_supp fin_supp fresh_prod fresh_atm cmaps_fresh)
  apply(simp)
  apply(case_tac "findn θ_n name2")
   apply(auto simp add: abs_fresh)[1]
  apply(auto)[1]
  apply(generate_fresh "name")
  apply(fresh_fun_simp)
  apply(simp add: abs_fresh fresh_prod fresh_atm nmaps_fresh)
  done

lemma psubst_csubst:
  assumes a: "a♯(θ_n,θ_c)"
  shows "θ_n,((a,x,P)#θ_c)<M> = ((θ_n,θ_c<M>){a:=(x).P})"
  using a
  apply(nominal_induct M avoiding: a x θ_n θ_c P rule: trm.strong_induct)
             apply(auto simp add: fresh_list_cons fresh_prod)[1]
             apply(simp add: lookup_csubst)
            apply(simp add: fresh_list_cons fresh_prod)
            apply(auto)[1]
                 apply(rule sym)
                 apply(rule trans)
                  apply(rule better_Cut_substc)
                   apply(simp)
                  apply(simp add: abs_fresh fresh_atm)
                 apply(simp add: lookupd_fresh)
                 apply(subgoal_tac "a♯lookupc xa coname θ_n")
                  apply(simp add: forget)
                  apply(simp add: trm.inject)
                  apply(rule sym)
                  apply(simp add: alpha nrename_swap fresh_atm)
                 apply(rule lookupc_freshness)
                 apply(simp add: fresh_atm)
                apply(rule sym)
                apply(rule trans)
                 apply(rule better_Cut_substc)
                  apply(simp)
                 apply(simp add: abs_fresh fresh_atm)
                apply(simp)
                apply(rule conjI)
                 apply(rule impI)
                 apply(simp add: lookupd_unicity)
                apply(rule impI)
                apply(subgoal_tac "a♯lookupc xa coname θ_n")
                 apply(subgoal_tac "a♯lookupd name aa θ_c")
                  apply(simp add: forget)
                 apply(rule lookupd_freshness)
                 apply(simp add: fresh_atm)
                apply(rule lookupc_freshness)
                apply(simp add: fresh_atm)
               apply(rule sym)
               apply(rule trans)
                apply(rule better_Cut_substc)
                 apply(simp)
                apply(simp add: abs_fresh fresh_atm)
               apply(simp)
               apply(rule conjI)
                apply(rule impI)
                apply(drule ax_psubst)
                  apply(simp)
                 apply(simp)
                apply(blast)
               apply(rule impI)
               apply(subgoal_tac "a♯lookupc xa coname θ_n")
                apply(simp add: forget)
               apply(rule lookupc_freshness)
               apply(simp add: fresh_atm)
              apply(rule sym)
              apply(rule trans)
               apply(rule better_Cut_substc)
                apply(simp)
               apply(simp add: abs_fresh fresh_atm)
              apply(simp)
              apply(rule conjI)
               apply(rule impI)
               apply(simp add: trm.inject)
               apply(rule sym)
               apply(simp add: alpha)
               apply(simp add: alpha nrename_swap fresh_atm)
              apply(simp add: lookupd_fresh)
             apply(rule sym)
             apply(rule trans)
              apply(rule better_Cut_substc)
               apply(simp)
              apply(simp add: abs_fresh fresh_atm)
             apply(simp)
             apply(rule conjI)
              apply(rule impI)
              apply(simp add: lookupd_unicity)
             apply(rule impI)
             apply(subgoal_tac "a♯lookupd name aa θ_c")
              apply(simp add: forget)
             apply(rule lookupd_freshness)
             apply(simp add: fresh_atm)
            apply(rule sym)
            apply(rule trans)
             apply(rule better_Cut_substc)
              apply(simp)
             apply(simp add: abs_fresh fresh_atm)
            apply(simp)
            apply(rule impI)
            apply(drule ax_psubst)
              apply(simp)
             apply(simp)
            apply(blast)
    (* NotR *)
           apply(simp)
           apply(case_tac "findc θ_c coname")
            apply(simp)
            apply(auto simp add: fresh_list_cons fresh_prod)[1]
           apply(simp)
           apply(auto simp add: fresh_list_cons fresh_prod)[1]
            apply(drule cmaps_false)
             apply(assumption)
            apply(simp)
           apply(generate_fresh "coname")
           apply(fresh_fun_simp)
           apply(fresh_fun_simp)
           apply(rule sym)
           apply(rule trans)
            apply(rule better_Cut_substc1)
             apply(simp)
            apply(simp add: cmaps_fresh)
           apply(auto simp add: fresh_prod fresh_atm)[1]
    (* NotL *)
          apply(simp)
          apply(case_tac "findn θ_n name")
           apply(simp)
           apply(auto simp add: fresh_list_cons fresh_prod)[1]
          apply(simp)
          apply(auto simp add: fresh_list_cons fresh_prod)[1]
          apply(generate_fresh "name")
          apply(fresh_fun_simp)
          apply(fresh_fun_simp)
          apply(drule_tac a="a" in nmaps_fresh)
           apply(assumption)
          apply(rule sym)
          apply(rule trans)
           apply(rule better_Cut_substc2)
             apply(simp)
            apply(simp)
           apply(simp)
          apply(simp)
    (* AndR *)
         apply(simp)
         apply(case_tac "findc θ_c coname3")
          apply(simp)
          apply(auto simp add: psubst_fresh_coname fresh_list_cons fresh_prod fresh_atm)[1]
         apply(simp)
         apply(auto simp add: fresh_list_cons fresh_prod)[1]
          apply(drule cmaps_false)
           apply(assumption)
          apply(simp)
         apply(generate_fresh "coname")
         apply(fresh_fun_simp)
         apply(fresh_fun_simp)
         apply(rule sym)
         apply(rule trans)
          apply(rule better_Cut_substc1)
           apply(simp)
          apply(simp add: cmaps_fresh)
         apply(auto simp add:  psubst_fresh_coname fresh_prod fresh_atm)[1]
    (* AndL1 *)
        apply(simp)
        apply(case_tac "findn θ_n name2")
         apply(simp)
         apply(auto simp add: fresh_list_cons fresh_prod)[1]
        apply(simp)
        apply(auto simp add: fresh_list_cons fresh_prod)[1]
        apply(generate_fresh "name")
        apply(fresh_fun_simp)
        apply(fresh_fun_simp)
        apply(drule_tac a="a" in nmaps_fresh)
         apply(assumption)
        apply(rule sym)
        apply(rule trans)
         apply(rule better_Cut_substc2)
           apply(simp)
          apply(simp)
         apply(simp)
        apply(auto simp add:  psubst_fresh_coname fresh_prod fresh_atm)[1]
    (* AndL2 *)
       apply(simp)
       apply(case_tac "findn θ_n name2")
        apply(simp)
        apply(auto simp add: fresh_list_cons fresh_prod)[1]
       apply(simp)
       apply(auto simp add: fresh_list_cons fresh_prod)[1]
       apply(generate_fresh "name")
       apply(fresh_fun_simp)
       apply(fresh_fun_simp)
       apply(drule_tac a="a" in nmaps_fresh)
        apply(assumption)
       apply(rule sym)
       apply(rule trans)
        apply(rule better_Cut_substc2)
          apply(simp)
         apply(simp)
        apply(simp)
       apply(auto simp add:  psubst_fresh_coname fresh_prod fresh_atm)[1]
    (* OrR1 *)
      apply(simp)
      apply(case_tac "findc θ_c coname2")
       apply(simp)
       apply(auto simp add: psubst_fresh_coname fresh_list_cons fresh_prod fresh_atm)[1]
      apply(simp)
      apply(auto simp add: fresh_list_cons fresh_prod)[1]
       apply(drule cmaps_false)
        apply(assumption)
       apply(simp)
      apply(generate_fresh "coname")
      apply(fresh_fun_simp)
      apply(fresh_fun_simp)
      apply(rule sym)
      apply(rule trans)
       apply(rule better_Cut_substc1)
        apply(simp)
       apply(simp add: cmaps_fresh)
      apply(auto simp add:  psubst_fresh_coname fresh_prod fresh_atm)[1]
    (* OrR2 *)
     apply(simp)
     apply(case_tac "findc θ_c coname2")
      apply(simp)
      apply(auto simp add: psubst_fresh_coname fresh_list_cons fresh_prod fresh_atm)[1]
     apply(simp)
     apply(auto simp add: fresh_list_cons fresh_prod)[1]
      apply(drule cmaps_false)
       apply(assumption)
      apply(simp)
     apply(generate_fresh "coname")
     apply(fresh_fun_simp)
     apply(fresh_fun_simp)
     apply(rule sym)
     apply(rule trans)
      apply(rule better_Cut_substc1)
       apply(simp)
      apply(simp add: cmaps_fresh)
     apply(auto simp add:  psubst_fresh_coname fresh_prod fresh_atm)[1]
    (* OrL *)
    apply(simp)
    apply(case_tac "findn θ_n name3")
     apply(simp)
     apply(auto simp add: fresh_list_cons psubst_fresh_name fresh_atm fresh_prod)[1]
    apply(simp)
    apply(auto simp add: fresh_list_cons fresh_prod)[1]
    apply(generate_fresh "name")
    apply(fresh_fun_simp)
    apply(fresh_fun_simp)
    apply(drule_tac a="a" in nmaps_fresh)
     apply(assumption)
    apply(rule sym)
    apply(rule trans)
     apply(rule better_Cut_substc2)
       apply(simp)
      apply(simp)
     apply(simp)
    apply(auto simp add:  psubst_fresh_name fresh_prod fresh_atm)[1]
    (* ImpR *)
   apply(simp)
   apply(case_tac "findc θ_c coname2")
    apply(simp)
    apply(auto simp add: psubst_fresh_coname fresh_list_cons fresh_prod fresh_atm)[1]
   apply(simp)
   apply(auto simp add: fresh_list_cons fresh_prod)[1]
    apply(drule cmaps_false)
     apply(assumption)
    apply(simp)
   apply(generate_fresh "coname")
   apply(fresh_fun_simp)
   apply(fresh_fun_simp)
   apply(rule sym)
   apply(rule trans)
    apply(rule better_Cut_substc1)
     apply(simp)
    apply(simp add: cmaps_fresh)
   apply(auto simp add:  psubst_fresh_coname fresh_prod fresh_atm)[1]
    (* ImpL *)
  apply(simp)
  apply(case_tac "findn θ_n name2")
   apply(simp)
   apply(auto simp add: fresh_list_cons psubst_fresh_coname psubst_fresh_name fresh_atm fresh_prod)[1]
  apply(simp)
  apply(auto simp add: fresh_list_cons fresh_prod)[1]
  apply(generate_fresh "name")
  apply(fresh_fun_simp)
  apply(fresh_fun_simp)
  apply(simp add: abs_fresh subst_fresh)
  apply(drule_tac a="a" in nmaps_fresh)
   apply(assumption)
  apply(rule sym)
  apply(rule trans)
   apply(rule better_Cut_substc2)
     apply(simp)
    apply(simp)
   apply(simp)
  apply(auto simp add: psubst_fresh_coname psubst_fresh_name fresh_prod fresh_atm)[1]
  done

lemma psubst_nsubst:
  assumes a: "x♯(θ_n,θ_c)"
  shows "((x,a,P)#θ_n),θ_c<M> = ((θ_n,θ_c<M>){x:=<a>.P})"
  using a
  apply(nominal_induct M avoiding: a x θ_n θ_c P rule: trm.strong_induct)
             apply(auto simp add: fresh_list_cons fresh_prod)[1]
              apply(simp add: lookup_fresh)
              apply(rule lookupb_lookupa)
              apply(simp)
             apply(rule sym)
             apply(rule forget)
             apply(rule lookup_freshness)
             apply(simp add: fresh_atm)
            apply(auto simp add: lookupc_freshness fresh_list_cons fresh_prod)[1]
                 apply(simp add: lookupc_fresh)
                 apply(rule sym)
                 apply(rule trans)
                  apply(rule better_Cut_substn)
                   apply(simp add: abs_fresh)
                  apply(simp add: abs_fresh fresh_atm)
                 apply(simp add: lookupd_fresh)
                 apply(subgoal_tac "x♯lookupd name aa θ_c")
                  apply(simp add: forget)
                  apply(simp add: trm.inject)
                  apply(rule sym)
                  apply(simp add: alpha crename_swap fresh_atm)
                 apply(rule lookupd_freshness)
                 apply(simp add: fresh_atm)
                apply(rule sym)
                apply(rule trans)
                 apply(rule better_Cut_substn)
                  apply(simp add: abs_fresh) 
                 apply(simp add: abs_fresh fresh_atm)
                apply(simp)
                apply(rule conjI)
                 apply(rule impI)
                 apply(simp add: lookupc_unicity)
                apply(rule impI)
                apply(subgoal_tac "x♯lookupc xa coname θ_n")
                 apply(subgoal_tac "x♯lookupd name aa θ_c")
                  apply(simp add: forget)
                 apply(rule lookupd_freshness)
                 apply(simp add: fresh_atm)
                apply(rule lookupc_freshness)
                apply(simp add: fresh_atm)
               apply(rule sym)
               apply(rule trans)
                apply(rule better_Cut_substn)
                 apply(simp add: abs_fresh)
                apply(simp add: abs_fresh fresh_atm)
               apply(simp)
               apply(rule conjI)
                apply(rule impI)
                apply(simp add: trm.inject)
                apply(rule sym)
                apply(simp add: alpha crename_swap fresh_atm)
               apply(rule impI)
               apply(simp add: lookupc_fresh)
              apply(rule sym)
              apply(rule trans)
               apply(rule better_Cut_substn)
                apply(simp add: abs_fresh)
               apply(simp add: abs_fresh fresh_atm)
              apply(simp)
              apply(rule conjI)
               apply(rule impI)
               apply(simp add: lookupc_unicity)
              apply(rule impI)
              apply(subgoal_tac "x♯lookupc xa coname θ_n")
               apply(simp add: forget)
              apply(rule lookupc_freshness)
              apply(simp add: fresh_prod fresh_atm)
             apply(rule sym)
             apply(rule trans)
              apply(rule better_Cut_substn)
               apply(simp add: abs_fresh)
              apply(simp add: abs_fresh fresh_atm)
             apply(simp)
             apply(rule conjI)
              apply(rule impI)
              apply(drule ax_psubst)
                apply(simp)
               apply(simp)
              apply(simp)
              apply(blast)
             apply(rule impI)
             apply(subgoal_tac "x♯lookupd name aa θ_c")
              apply(simp add: forget)
             apply(rule lookupd_freshness)
             apply(simp add: fresh_atm)
            apply(rule sym)
            apply(rule trans)
             apply(rule better_Cut_substn)
              apply(simp add: abs_fresh)
             apply(simp add: abs_fresh fresh_atm)
            apply(simp)
            apply(rule impI)
            apply(drule ax_psubst)
              apply(simp)
             apply(simp)
            apply(blast)
    (* NotR *)
           apply(simp)
           apply(case_tac "findc θ_c coname")
            apply(simp)
            apply(auto simp add: fresh_list_cons fresh_prod)[1]
           apply(simp)
           apply(auto simp add: fresh_list_cons fresh_prod)[1]
           apply(generate_fresh "coname")
           apply(fresh_fun_simp)
           apply(fresh_fun_simp)
           apply(rule sym)
           apply(rule trans)
            apply(rule better_Cut_substn1)
              apply(simp add: cmaps_fresh)
             apply(simp)
            apply(simp)
           apply(simp)
    (* NotL *)
          apply(simp)
          apply(case_tac "findn θ_n name")
           apply(simp)
           apply(auto simp add: fresh_list_cons fresh_prod)[1]
          apply(simp)
          apply(auto simp add: fresh_list_cons fresh_prod)[1]
           apply(drule nmaps_false)
            apply(simp)
           apply(simp)
          apply(generate_fresh "name")
          apply(fresh_fun_simp)
          apply(fresh_fun_simp)
          apply(rule sym)
          apply(rule trans)
           apply(rule better_Cut_substn2)
            apply(simp)
           apply(simp add: nmaps_fresh)
          apply(simp add: fresh_prod fresh_atm)
    (* AndR *)
         apply(simp)
         apply(case_tac "findc θ_c coname3")
          apply(simp)
          apply(auto simp add: psubst_fresh_coname fresh_list_cons fresh_prod fresh_atm)[1]
         apply(simp)
         apply(auto simp add: fresh_list_cons fresh_prod)[1]
         apply(generate_fresh "coname")
         apply(fresh_fun_simp)
         apply(fresh_fun_simp)
         apply(rule sym)
         apply(rule trans)
          apply(rule better_Cut_substn1)
            apply(simp add: cmaps_fresh)
           apply(simp)
          apply(simp)
         apply(auto simp add:  psubst_fresh_coname fresh_prod fresh_atm)[1]
    (* AndL1 *)
        apply(simp)
        apply(case_tac "findn θ_n name2")
         apply(simp)
         apply(auto simp add: fresh_list_cons fresh_prod)[1]
        apply(simp)
        apply(auto simp add: fresh_list_cons fresh_prod)[1]
         apply(drule nmaps_false)
          apply(simp)
         apply(simp)
        apply(generate_fresh "name")
        apply(fresh_fun_simp)
        apply(fresh_fun_simp)
        apply(rule sym)
        apply(rule trans)
         apply(rule better_Cut_substn2)
          apply(simp)
         apply(simp add: nmaps_fresh)
        apply(auto simp add:  psubst_fresh_coname fresh_prod fresh_atm)[1]
    (* AndL2 *)
       apply(simp)
       apply(case_tac "findn θ_n name2")
        apply(simp)
        apply(auto simp add: fresh_list_cons fresh_prod)[1]
       apply(simp)
       apply(auto simp add: fresh_list_cons fresh_prod)[1]
        apply(drule nmaps_false)
         apply(simp)
        apply(simp)
       apply(generate_fresh "name")
       apply(fresh_fun_simp)
       apply(fresh_fun_simp)
       apply(rule sym)
       apply(rule trans)
        apply(rule better_Cut_substn2)
         apply(simp)
        apply(simp add: nmaps_fresh)
       apply(auto simp add:  psubst_fresh_coname fresh_prod fresh_atm)[1]
    (* OrR1 *)
      apply(simp)
      apply(case_tac "findc θ_c coname2")
       apply(simp)
       apply(auto simp add: psubst_fresh_coname fresh_list_cons fresh_prod fresh_atm)[1]
      apply(simp)
      apply(auto simp add: fresh_list_cons fresh_prod)[1]
      apply(generate_fresh "coname")
      apply(fresh_fun_simp)
      apply(fresh_fun_simp)
      apply(rule sym)
      apply(rule trans)
       apply(rule better_Cut_substn1)
         apply(simp add: cmaps_fresh)
        apply(simp)
       apply(simp)
      apply(auto simp add:  psubst_fresh_coname fresh_prod fresh_atm)[1]
    (* OrR2 *)
     apply(simp)
     apply(case_tac "findc θ_c coname2")
      apply(simp)
      apply(auto simp add: psubst_fresh_coname fresh_list_cons fresh_prod fresh_atm)[1]
     apply(simp)
     apply(auto simp add: fresh_list_cons fresh_prod)[1]
     apply(generate_fresh "coname")
     apply(fresh_fun_simp)
     apply(fresh_fun_simp)
     apply(rule sym)
     apply(rule trans)
      apply(rule better_Cut_substn1)
        apply(simp add: cmaps_fresh)
       apply(simp)
      apply(simp)
     apply(auto simp add:  psubst_fresh_coname fresh_prod fresh_atm)[1]
    (* OrL *)
    apply(simp)
    apply(case_tac "findn θ_n name3")
     apply(simp)
     apply(auto simp add: fresh_list_cons psubst_fresh_name fresh_atm fresh_prod)[1]
    apply(simp)
    apply(auto simp add: fresh_list_cons fresh_prod)[1]
     apply(drule nmaps_false)
      apply(simp)
     apply(simp)
    apply(generate_fresh "name")
    apply(fresh_fun_simp)
    apply(fresh_fun_simp)
    apply(rule sym)
    apply(rule trans)
     apply(rule better_Cut_substn2)
      apply(simp)
     apply(simp add: nmaps_fresh)
    apply(auto simp add:  psubst_fresh_name fresh_prod fresh_atm)[1]
    (* ImpR *)
   apply(simp)
   apply(case_tac "findc θ_c coname2")
    apply(simp)
    apply(auto simp add: psubst_fresh_coname fresh_list_cons fresh_prod fresh_atm)[1]
   apply(simp)
   apply(auto simp add: fresh_list_cons fresh_prod)[1]
   apply(generate_fresh "coname")
   apply(fresh_fun_simp)
   apply(fresh_fun_simp)
   apply(rule sym)
   apply(rule trans)
    apply(rule better_Cut_substn1)
      apply(simp add: cmaps_fresh)
     apply(simp)
    apply(simp)
   apply(auto simp add:  psubst_fresh_coname fresh_prod fresh_atm)[1]
    (* ImpL *)
  apply(simp)
  apply(case_tac "findn θ_n name2")
   apply(simp)
   apply(auto simp add: fresh_list_cons psubst_fresh_coname psubst_fresh_name fresh_atm fresh_prod)[1]
  apply(simp)
  apply(auto simp add: fresh_list_cons fresh_prod)[1]
   apply(drule nmaps_false)
    apply(simp)
   apply(simp)
  apply(generate_fresh "name")
  apply(fresh_fun_simp)
  apply(fresh_fun_simp)
  apply(rule sym)
  apply(rule trans)
   apply(rule better_Cut_substn2)
    apply(simp)
   apply(simp add: nmaps_fresh)
  apply(auto simp add: psubst_fresh_coname psubst_fresh_name fresh_prod fresh_atm)[1]
  done

definition 
  ncloses :: "(name×coname×trm) list⇒(name×ty) list ⇒ bool" (‹_ ncloses _› [55,55] 55) 
  where
    "θ_n ncloses Γ ≡ ∀x B. ((x,B) ∈ set Γ ⟶ (∃c P. θ_n nmaps x to Some (c,P) ∧ <c>:P ∈ (∥<B>∥)))"

definition 
  ccloses :: "(coname×name×trm) list⇒(coname×ty) list ⇒ bool" (‹_ ccloses _› [55,55] 55) 
  where
    "θ_c ccloses Δ ≡ ∀a B. ((a,B) ∈ set Δ ⟶ (∃x P. θ_c cmaps a to Some (x,P) ∧ (x):P ∈ (∥(B)∥)))"

lemma ncloses_elim:
  assumes a: "(x,B) ∈ set Γ"
    and     b: "θ_n ncloses Γ"
  shows "∃c P. θ_n nmaps x to Some (c,P) ∧ <c>:P ∈ (∥<B>∥)"
  using a b by (auto simp add: ncloses_def)

lemma ccloses_elim:
  assumes a: "(a,B) ∈ set Δ"
    and     b: "θ_c ccloses Δ"
  shows "∃x P. θ_c cmaps a to Some (x,P) ∧ (x):P ∈ (∥(B)∥)"
  using a b by (auto simp add: ccloses_def)

lemma ncloses_subset:
  assumes a: "θ_n ncloses Γ"
    and     b: "set Γ' ⊆ set Γ"
  shows "θ_n ncloses Γ'"
  using a b by (auto  simp add: ncloses_def)

lemma ccloses_subset:
  assumes a: "θ_c ccloses Δ"
    and     b: "set Δ' ⊆ set Δ"
  shows "θ_c ccloses Δ'"
  using a b by (auto  simp add: ccloses_def)

lemma validc_fresh:
  fixes a::"coname"
    and   Δ::"(coname×ty) list"
  assumes a: "a♯Δ"
  shows "¬(∃B. (a,B)∈set Δ)"
  using a
  apply(induct Δ)
   apply(auto simp add: fresh_list_cons fresh_prod fresh_atm)
  done

lemma validn_fresh:
  fixes x::"name"
    and   Γ::"(name×ty) list"
  assumes a: "x♯Γ"
  shows "¬(∃B. (x,B)∈set Γ)"
  using a
  apply(induct Γ)
   apply(auto simp add: fresh_list_cons fresh_prod fresh_atm)
  done

lemma ccloses_extend:
  assumes a: "θ_c ccloses Δ" "a♯Δ" "a♯θ_c" "(x):P∈∥(B)∥"
  shows "(a,x,P)#θ_c ccloses (a,B)#Δ"
  using a
  apply(simp add: ccloses_def)
  apply(drule validc_fresh)
  apply(auto)
  done

lemma ncloses_extend:
  assumes a: "θ_n ncloses Γ" "x♯Γ" "x♯θ_n" "<a>:P∈∥<B>∥"
  shows "(x,a,P)#θ_n ncloses (x,B)#Γ"
  using a
  apply(simp add: ncloses_def)
  apply(drule validn_fresh)
  apply(auto)
  done


text ‹typing relation›

inductive
  typing :: "ctxtn ⇒ trm ⇒ ctxtc ⇒ bool" (‹_ ⊢ _ ⊢ _› [100,100,100] 100)
  where
    TAx:    "⟦validn Γ;validc Δ; (x,B)∈set Γ; (a,B)∈set Δ⟧ ⟹ Γ ⊢ Ax x a ⊢ Δ"
  | TNotR:  "⟦x♯Γ; ((x,B)#Γ) ⊢ M ⊢ Δ; set Δ' = {(a,NOT B)}∪set Δ; validc Δ'⟧ 
           ⟹ Γ ⊢ NotR (x).M a ⊢ Δ'"
  | TNotL:  "⟦a♯Δ; Γ ⊢ M ⊢ ((a,B)#Δ); set Γ' = {(x,NOT B)} ∪ set Γ; validn Γ'⟧  
           ⟹ Γ' ⊢ NotL <a>.M x ⊢ Δ"
  | TAndL1: "⟦x♯(Γ,y); ((x,B1)#Γ) ⊢ M ⊢ Δ; set Γ' = {(y,B1 AND B2)} ∪ set Γ; validn Γ'⟧ 
           ⟹ Γ' ⊢ AndL1 (x).M y ⊢ Δ"
  | TAndL2: "⟦x♯(Γ,y); ((x,B2)#Γ) ⊢ M ⊢ Δ; set Γ' = {(y,B1 AND B2)} ∪ set Γ; validn Γ'⟧ 
           ⟹ Γ' ⊢ AndL2 (x).M y ⊢ Δ"
  | TAndR:  "⟦a♯(Δ,N,c); b♯(Δ,M,c); a≠b; Γ ⊢ M ⊢ ((a,B)#Δ); Γ ⊢ N ⊢ ((b,C)#Δ); 
           set Δ' = {(c,B AND C)}∪set Δ; validc Δ'⟧ 
           ⟹ Γ ⊢ AndR <a>.M <b>.N c ⊢ Δ'"
  | TOrL:   "⟦x♯(Γ,N,z); y♯(Γ,M,z); x≠y; ((x,B)#Γ) ⊢ M ⊢ Δ; ((y,C)#Γ) ⊢ N ⊢ Δ;
           set Γ' = {(z,B OR C)} ∪ set Γ; validn Γ'⟧ 
           ⟹ Γ' ⊢ OrL (x).M (y).N z ⊢ Δ"
  | TOrR1:  "⟦a♯(Δ,b); Γ ⊢ M ⊢ ((a,B1)#Δ); set Δ' = {(b,B1 OR B2)}∪set Δ; validc Δ'⟧ 
           ⟹ Γ ⊢ OrR1 <a>.M b ⊢ Δ'"
  | TOrR2:  "⟦a♯(Δ,b); Γ ⊢ M ⊢ ((a,B2)#Δ); set Δ' = {(b,B1 OR B2)}∪set Δ; validc Δ'⟧ 
           ⟹ Γ ⊢ OrR2 <a>.M b ⊢ Δ'"
  | TImpL:  "⟦a♯(Δ,N); x♯(Γ,M,y); Γ ⊢ M ⊢ ((a,B)#Δ); ((x,C)#Γ) ⊢ N ⊢ Δ;
           set Γ' = {(y,B IMP C)} ∪ set Γ; validn Γ'⟧ 
           ⟹ Γ' ⊢ ImpL <a>.M (x).N y ⊢ Δ"
  | TImpR:  "⟦a♯(Δ,b); x♯Γ; ((x,B)#Γ) ⊢ M ⊢ ((a,C)#Δ); set Δ' = {(b,B IMP C)}∪set Δ; validc Δ'⟧ 
           ⟹ Γ ⊢ ImpR (x).<a>.M b ⊢ Δ'"
  | TCut:   "⟦a♯(Δ,N); x♯(Γ,M); Γ ⊢ M ⊢ ((a,B)#Δ); ((x,B)#Γ) ⊢ N ⊢ Δ⟧ 
           ⟹ Γ ⊢ Cut <a>.M (x).N ⊢ Δ"

equivariance typing

lemma fresh_set_member:
  fixes x::"name"
    and   a::"coname"
  shows "x♯L ⟹ e∈set L ⟹ x♯e"
    and   "a♯L ⟹ e∈set L ⟹ a♯e"   
  by (induct L) (auto simp add: fresh_list_cons) 

lemma fresh_subset:
  fixes x::"name"
    and   a::"coname"
  shows "x♯L ⟹ set L' ⊆ set L ⟹ x♯L'"
    and   "a♯L ⟹ set L' ⊆ set L ⟹ a♯L'"   
   apply(induct L' arbitrary: L) 
     apply(auto simp add: fresh_list_cons fresh_list_nil intro: fresh_set_member)
  done

lemma fresh_subset_ext:
  fixes x::"name"
    and   a::"coname"
  shows "x♯L ⟹ x♯e ⟹ set L' ⊆ set (e#L) ⟹ x♯L'"
    and   "a♯L ⟹ a♯e ⟹ set L' ⊆ set (e#L) ⟹ a♯L'"   
   apply(induct L' arbitrary: L) 
     apply(auto simp add: fresh_list_cons fresh_list_nil intro: fresh_set_member)
  done

lemma fresh_under_insert:
  fixes x::"name"
    and   a::"coname"
    and   Γ::"ctxtn"
    and   Δ::"ctxtc"
  shows "x♯Γ ⟹ x≠y ⟹ set Γ' = insert (y,B) (set Γ) ⟹ x♯Γ'"
    and   "a♯Δ ⟹ a≠c ⟹ set Δ' = insert (c,B) (set Δ) ⟹ a♯Δ'"   
   apply(rule fresh_subset_ext(1))
     apply(auto simp add: fresh_prod fresh_atm fresh_ty)
  apply(rule fresh_subset_ext(2))
    apply(auto simp add: fresh_prod fresh_atm fresh_ty)
  done

nominal_inductive typing
                       apply (simp_all add: abs_fresh fresh_atm fresh_list_cons fresh_prod fresh_ty fresh_ctxt 
      fresh_list_append abs_supp fin_supp)
           apply(auto intro: fresh_under_insert)
  done

lemma validn_elim:
  assumes a: "validn ((x,B)#Γ)"
  shows "validn Γ ∧ x♯Γ"
  using a
  apply(erule_tac validn.cases)
   apply(auto)
  done

lemma validc_elim:
  assumes a: "validc ((a,B)#Δ)"
  shows "validc Δ ∧ a♯Δ"
  using a
  apply(erule_tac validc.cases)
   apply(auto)
  done

lemma context_fresh:
  fixes x::"name"
    and   a::"coname"
  shows "x♯Γ ⟹ ¬(∃B. (x,B)∈set Γ)"
    and   "a♯Δ ⟹ ¬(∃B. (a,B)∈set Δ)"
   apply -
   apply(induct Γ)
    apply(auto simp add: fresh_list_cons fresh_prod fresh_atm)
  apply(induct Δ)
   apply(auto simp add: fresh_list_cons fresh_prod fresh_atm)
  done

lemma typing_implies_valid:
  assumes a: "Γ ⊢ M ⊢ Δ"
  shows "validn Γ ∧ validc Δ"
  using a
  apply(nominal_induct rule: typing.strong_induct)
             apply(auto dest: validn_elim validc_elim)
  done

lemma ty_perm:
  fixes pi1::"name prm"
    and   pi2::"coname prm"
    and   B::"ty"
  shows "pi1∙B=B" and "pi2∙B=B"
   apply(nominal_induct B rule: ty.strong_induct)
           apply(auto simp add: perm_string)
  done

lemma ctxt_perm:
  fixes pi1::"name prm"
    and   pi2::"coname prm"
    and   Γ::"ctxtn"
    and   Δ::"ctxtc"
  shows "pi2∙Γ=Γ" and "pi1∙Δ=Δ"
   apply -
   apply(induct Γ)
    apply(auto simp add: calc_atm ty_perm)
  apply(induct Δ)
   apply(auto simp add: calc_atm ty_perm)
  done

lemma typing_Ax_elim1: 
  assumes a: "Γ ⊢ Ax x a ⊢ ((a,B)#Δ)"
  shows "(x,B)∈set Γ"
  using a
  apply(erule_tac typing.cases)
             apply(simp_all add: trm.inject)
  apply(auto)
  apply(auto dest: validc_elim context_fresh)
  done

lemma typing_Ax_elim2: 
  assumes a: "((x,B)#Γ) ⊢ Ax x a ⊢ Δ"
  shows "(a,B)∈set Δ"
  using a
  apply(erule_tac typing.cases)
             apply(simp_all add: trm.inject)
  apply(auto  dest!: validn_elim context_fresh)
  done

lemma psubst_Ax_aux: 
  assumes a: "θ_c cmaps a to Some (y,N)"
  shows "lookupb x a θ_c c P = Cut <c>.P (y).N"
  using a
  apply(induct θ_c)
   apply(auto)
  done

lemma psubst_Ax:
  assumes a: "θ_n nmaps x to Some (c,P)"
    and     b: "θ_c cmaps a to Some (y,N)"
  shows "θ_n,θ_c<Ax x a> = Cut <c>.P (y).N"
  using a b
  apply(induct θ_n)
   apply(auto simp add: psubst_Ax_aux)
  done

lemma psubst_Cut:
  assumes a: "∀x. M≠Ax x c"
    and     b: "∀a. N≠Ax x a"
    and     c: "c♯(θ_n,θ_c,N)" "x♯(θ_n,θ_c,M)"
  shows "θ_n,θ_c<Cut <c>.M (x).N> = Cut <c>.(θ_n,θ_c<M>) (x).(θ_n,θ_c<N>)"
  using a b c
  apply(simp)
  done

lemma all_CAND: 
  assumes a: "Γ ⊢ M ⊢ Δ"
    and     b: "θ_n ncloses Γ"
    and     c: "θ_c ccloses Δ"
  shows "SNa (θ_n,θ_c<M>)"
  using a b c
proof(nominal_induct avoiding: θ_n θ_c rule: typing.strong_induct)
  case (TAx Γ Δ x B a θ_n θ_c)
  then show ?case
    apply -
    apply(drule ncloses_elim)
     apply(assumption)
    apply(drule ccloses_elim)
     apply(assumption)
    apply(erule exE)+
    apply(erule conjE)+
    apply(rule_tac s="Cut <c>.P (xa).Pa" and t="θ_n,θ_c<Ax x a>" in subst)
     apply(rule sym)
     apply(simp only: psubst_Ax)
    apply(simp add: CUT_SNa)
    done
next
  case (TNotR x Γ B M Δ Δ' a θ_n θ_c) 
  then show ?case 
    apply(simp)
    apply(subgoal_tac "(a,NOT B) ∈ set Δ'")
     apply(drule ccloses_elim)
      apply(assumption)
     apply(erule exE)+
     apply(simp)
     apply(generate_fresh "coname")
     apply(fresh_fun_simp)
     apply(rule_tac B="NOT B" in CUT_SNa)
      apply(simp)
      apply(rule disjI2)
      apply(rule disjI2)
      apply(rule_tac x="c" in exI)
      apply(rule_tac x="x" in exI)
      apply(rule_tac x="θ_n,θ_c<M>" in exI)
      apply(simp)
      apply(rule conjI)
       apply(rule fic.intros)
       apply(rule psubst_fresh_coname)
         apply(simp)
        apply(simp)
       apply(simp)
      apply(rule BINDING_implies_CAND)
      apply(unfold BINDINGn_def)
      apply(simp)
      apply(rule_tac x="x" in exI)
      apply(rule_tac x="θ_n,θ_c<M>" in exI)
      apply(simp)
      apply(rule allI)+
      apply(rule impI)
      apply(simp add: psubst_nsubst[symmetric])
      apply(drule_tac x="(x,aa,Pa)#θ_n" in meta_spec)
      apply(drule_tac x="θ_c" in meta_spec)
      apply(drule meta_mp)
       apply(rule ncloses_extend)
          apply(assumption)
         apply(assumption)
        apply(assumption)
       apply(assumption)
      apply(drule meta_mp)
       apply(rule ccloses_subset)
        apply(assumption)
       apply(blast)
      apply(assumption)
     apply(simp)
    apply(blast)
    done
next
  case (TNotL a Δ Γ M B Γ' x θ_n θ_c)
  then show ?case
    apply(simp)
    apply(subgoal_tac "(x,NOT B) ∈ set Γ'")
     apply(drule ncloses_elim)
      apply(assumption)
     apply(erule exE)+
     apply(simp del: NEGc.simps)
     apply(generate_fresh "name")
     apply(fresh_fun_simp)
     apply(rule_tac B="NOT B" in CUT_SNa)
      apply(simp)
     apply(rule NEG_intro)
     apply(simp (no_asm))
     apply(rule disjI2)
     apply(rule disjI2)
     apply(rule_tac x="a" in exI)
     apply(rule_tac x="ca" in exI)
     apply(rule_tac x="θ_n,θ_c<M>" in exI)
     apply(simp del: NEGc.simps)
     apply(rule conjI)
      apply(rule fin.intros)
      apply(rule psubst_fresh_name)
        apply(simp)
       apply(simp)
      apply(simp)
     apply(rule BINDING_implies_CAND)
     apply(unfold BINDINGc_def)
     apply(simp (no_asm))
     apply(rule_tac x="a" in exI)
     apply(rule_tac x="θ_n,θ_c<M>" in exI)
     apply(simp (no_asm))
     apply(rule allI)+
     apply(rule impI)
     apply(simp del: NEGc.simps add: psubst_csubst[symmetric])
     apply(drule_tac x="θ_n" in meta_spec)
     apply(drule_tac x="(a,xa,Pa)#θ_c" in meta_spec)
     apply(drule meta_mp)
      apply(rule ncloses_subset)
       apply(assumption)
      apply(blast)
     apply(drule meta_mp)
      apply(rule ccloses_extend)
         apply(assumption)
        apply(assumption)
       apply(assumption)
      apply(assumption)
     apply(assumption)
    apply(blast)
    done
next
  case (TAndL1 x Γ y B1 M Δ Γ' B2 θ_n θ_c)
  then show ?case     
    apply(simp)
    apply(subgoal_tac "(y,B1 AND B2) ∈ set Γ'")
     apply(drule ncloses_elim)
      apply(assumption)
     apply(erule exE)+ 
     apply(simp del: NEGc.simps)
     apply(generate_fresh "name")
     apply(fresh_fun_simp)
     apply(rule_tac B="B1 AND B2" in CUT_SNa)
      apply(simp)
     apply(rule NEG_intro)
     apply(simp (no_asm))
     apply(rule disjI2)
     apply(rule disjI2)
     apply(rule disjI1)
     apply(rule_tac x="x" in exI)
     apply(rule_tac x="ca" in exI)
     apply(rule_tac x="θ_n,θ_c<M>" in exI)
     apply(simp del: NEGc.simps)
     apply(rule conjI)
      apply(rule fin.intros)
      apply(simp del: NEGc.simps add: abs_fresh fresh_prod fresh_atm)
      apply(rule psubst_fresh_name)
        apply(simp)
       apply(simp)
      apply(simp)
     apply(rule BINDING_implies_CAND)
     apply(unfold BINDINGn_def)
     apply(simp (no_asm))
     apply(rule_tac x="x" in exI)
     apply(rule_tac x="θ_n,θ_c<M>" in exI)
     apply(simp (no_asm))
     apply(rule allI)+
     apply(rule impI)
     apply(simp del: NEGc.simps add: psubst_nsubst[symmetric])
     apply(drule_tac x="(x,a,Pa)#θ_n" in meta_spec)
     apply(drule_tac x="θ_c" in meta_spec)
     apply(drule meta_mp)
      apply(rule ncloses_extend)
         apply(rule ncloses_subset)
          apply(assumption)
         apply(blast)
        apply(simp)
       apply(simp)
      apply(simp)
     apply(drule meta_mp)
      apply(assumption)
     apply(assumption)
    apply(blast)
    done
next
  case (TAndL2 x Γ y B2 M Δ Γ' B1 θ_n θ_c)
  then show ?case 
    apply(simp)
    apply(subgoal_tac "(y,B1 AND B2) ∈ set Γ'")
     apply(drule ncloses_elim)
      apply(assumption)
     apply(erule exE)+ 
     apply(simp del: NEGc.simps)
     apply(generate_fresh "name")
     apply(fresh_fun_simp)
     apply(rule_tac B="B1 AND B2" in CUT_SNa)
      apply(simp)
     apply(rule NEG_intro)
     apply(simp (no_asm))
     apply(rule disjI2)
     apply(rule disjI2)
     apply(rule disjI2)
     apply(rule_tac x="x" in exI)
     apply(rule_tac x="ca" in exI)
     apply(rule_tac x="θ_n,θ_c<M>" in exI)
     apply(simp del: NEGc.simps)
     apply(rule conjI)
      apply(rule fin.intros)
      apply(simp del: NEGc.simps add: abs_fresh fresh_prod fresh_atm)
      apply(rule psubst_fresh_name)
        apply(simp)
       apply(simp)
      apply(simp)
     apply(rule BINDING_implies_CAND)
     apply(unfold BINDINGn_def)
     apply(simp (no_asm))
     apply(rule_tac x="x" in exI)
     apply(rule_tac x="θ_n,θ_c<M>" in exI)
     apply(simp (no_asm))
     apply(rule allI)+
     apply(rule impI)
     apply(simp del: NEGc.simps add: psubst_nsubst[symmetric])
     apply(drule_tac x="(x,a,Pa)#θ_n" in meta_spec)
     apply(drule_tac x="θ_c" in meta_spec)
     apply(drule meta_mp)
      apply(rule ncloses_extend)
         apply(rule ncloses_subset)
          apply(assumption)
         apply(blast)
        apply(simp)
       apply(simp)
      apply(simp)
     apply(drule meta_mp)
      apply(assumption)
     apply(assumption)
    apply(blast)
    done
next
  case (TAndR a Δ N c b M Γ B C Δ' θ_n θ_c)
  then show ?case 
    apply(simp)
    apply(subgoal_tac "(c,B AND C) ∈ set Δ'")
     apply(drule ccloses_elim)
      apply(assumption)
     apply(erule exE)+
     apply(simp)
     apply(generate_fresh "coname")
     apply(fresh_fun_simp)
     apply(rule_tac B="B AND C" in CUT_SNa)
      apply(simp)
      apply(rule disjI2)
      apply(rule disjI2)
      apply(rule_tac x="ca" in exI)
      apply(rule_tac x="a" in exI)
      apply(rule_tac x="b" in exI)
      apply(rule_tac x="θ_n,θ_c<M>" in exI)
      apply(rule_tac x="θ_n,θ_c<N>" in exI)
      apply(simp)
      apply(rule conjI)
       apply(rule fic.intros)
        apply(simp add: abs_fresh fresh_prod fresh_atm)
        apply(rule psubst_fresh_coname)
          apply(simp)
         apply(simp)
        apply(simp)
       apply(simp add: abs_fresh fresh_prod fresh_atm)
       apply(rule psubst_fresh_coname)
         apply(simp)
        apply(simp)
       apply(simp)
      apply(rule conjI)
       apply(rule BINDING_implies_CAND)
       apply(unfold BINDINGc_def)
       apply(simp)
       apply(rule_tac x="a" in exI)
       apply(rule_tac x="θ_n,θ_c<M>" in exI)
       apply(simp)
       apply(rule allI)+
       apply(rule impI)
       apply(simp add: psubst_csubst[symmetric])
       apply(drule_tac x="θ_n" in meta_spec)
       apply(drule_tac x="(a,xa,Pa)#θ_c" in meta_spec)
       apply(drule meta_mp)
        apply(assumption)
       apply(drule meta_mp)
        apply(rule ccloses_extend)
           apply(rule ccloses_subset)
            apply(assumption)
           apply(blast)
          apply(simp)
         apply(simp)
        apply(assumption)
       apply(assumption)
      apply(rule BINDING_implies_CAND)
      apply(unfold BINDINGc_def)
      apply(simp)
      apply(rule_tac x="b" in exI)
      apply(rule_tac x="θ_n,θ_c<N>" in exI)
      apply(simp)
      apply(rule allI)+
      apply(rule impI)
      apply(simp add: psubst_csubst[symmetric])
      apply(rotate_tac 14)
      apply(drule_tac x="θ_n" in meta_spec)
      apply(drule_tac x="(b,xa,Pa)#θ_c" in meta_spec)
      apply(drule meta_mp)
       apply(assumption)
      apply(drule meta_mp)
       apply(rule ccloses_extend)
          apply(rule ccloses_subset)
           apply(assumption)
          apply(blast)
         apply(simp)
        apply(simp)
       apply(assumption)
      apply(assumption)
     apply(simp)
    apply(blast)
    done
next
  case (TOrL x Γ N z y M B Δ C Γ' θ_n θ_c)
  then show ?case 
    apply(simp)
    apply(subgoal_tac "(z,B OR C) ∈ set Γ'")
     apply(drule ncloses_elim)
      apply(assumption)
     apply(erule exE)+
     apply(simp del: NEGc.simps)
     apply(generate_fresh "name")
     apply(fresh_fun_simp)
     apply(rule_tac B="B OR C" in CUT_SNa)
      apply(simp)
     apply(rule NEG_intro)
     apply(simp (no_asm))
     apply(rule disjI2)
     apply(rule disjI2)
     apply(rule_tac x="x" in exI)
     apply(rule_tac x="y" in exI)
     apply(rule_tac x="ca" in exI)
     apply(rule_tac x="θ_n,θ_c<M>" in exI)
     apply(rule_tac x="θ_n,θ_c<N>" in exI)
     apply(simp del: NEGc.simps)
     apply(rule conjI)
      apply(rule fin.intros)
       apply(simp del: NEGc.simps add: abs_fresh fresh_prod fresh_atm)
       apply(rule psubst_fresh_name)
         apply(simp)
        apply(simp)
       apply(simp)
      apply(simp del: NEGc.simps add: abs_fresh fresh_prod fresh_atm)
      apply(rule psubst_fresh_name)
        apply(simp)
       apply(simp)
      apply(simp)
     apply(rule conjI)
      apply(rule BINDING_implies_CAND)
      apply(unfold BINDINGn_def)
      apply(simp del: NEGc.simps)
      apply(rule_tac x="x" in exI)
      apply(rule_tac x="θ_n,θ_c<M>" in exI)
      apply(simp del: NEGc.simps)
      apply(rule allI)+
      apply(rule impI)
      apply(simp del: NEGc.simps add: psubst_nsubst[symmetric])
      apply(drule_tac x="(x,a,Pa)#θ_n" in meta_spec)
      apply(drule_tac x="θ_c" in meta_spec)
      apply(drule meta_mp)
       apply(rule ncloses_extend)
          apply(rule ncloses_subset)
           apply(assumption)
          apply(blast)
         apply(simp)
        apply(simp)
       apply(assumption)
      apply(drule meta_mp)
       apply(assumption)
      apply(assumption)
     apply(rule BINDING_implies_CAND)
     apply(unfold BINDINGn_def)
     apply(simp del: NEGc.simps)
     apply(rule_tac x="y" in exI)
     apply(rule_tac x="θ_n,θ_c<N>" in exI)
     apply(simp del: NEGc.simps)
     apply(rule allI)+
     apply(rule impI)
     apply(simp del: NEGc.simps add: psubst_nsubst[symmetric])
     apply(rotate_tac 14)
     apply(drule_tac x="(y,a,Pa)#θ_n" in meta_spec)
     apply(drule_tac x="θ_c" in meta_spec)
     apply(drule meta_mp)
      apply(rule ncloses_extend)
         apply(rule ncloses_subset)
          apply(assumption)
         apply(blast)
        apply(simp)
       apply(simp)
      apply(assumption)
     apply(drule meta_mp)
      apply(assumption)
     apply(assumption)
    apply(blast)
    done
next
  case (TOrR1 a Δ b Γ M B1 Δ' B2 θ_n θ_c)
  then show ?case
    apply(simp)
    apply(subgoal_tac "(b,B1 OR B2) ∈ set Δ'")
     apply(drule ccloses_elim)
      apply(assumption)
     apply(erule exE)+ 
     apply(simp del: NEGc.simps)
     apply(generate_fresh "coname")
     apply(fresh_fun_simp)
     apply(rule_tac B="B1 OR B2" in CUT_SNa)
      apply(simp)
      apply(rule disjI2)
      apply(rule disjI2)
      apply(rule disjI1)
      apply(rule_tac x="a" in exI)
      apply(rule_tac x="c" in exI)
      apply(rule_tac x="θ_n,θ_c<M>" in exI)
      apply(simp)
      apply(rule conjI)
       apply(rule fic.intros)
       apply(simp del: NEGc.simps add: abs_fresh fresh_prod fresh_atm)
       apply(rule psubst_fresh_coname)
         apply(simp)
        apply(simp)
       apply(simp)
      apply(rule BINDING_implies_CAND)
      apply(unfold BINDINGc_def)
      apply(simp (no_asm))
      apply(rule_tac x="a" in exI)
      apply(rule_tac x="θ_n,θ_c<M>" in exI)
      apply(simp (no_asm))
      apply(rule allI)+
      apply(rule impI)    
      apply(simp del: NEGc.simps add: psubst_csubst[symmetric])
      apply(drule_tac x="θ_n" in meta_spec)
      apply(drule_tac x="(a,xa,Pa)#θ_c" in meta_spec)
      apply(drule meta_mp)
       apply(assumption)
      apply(drule meta_mp)
       apply(rule ccloses_extend)
          apply(rule ccloses_subset)
           apply(assumption)
          apply(blast)
         apply(simp)
        apply(simp)
       apply(simp)
      apply(assumption)
     apply(simp)
    apply(blast)
    done
next
  case (TOrR2 a Δ b Γ M B2 Δ' B1 θ_n θ_c)
  then show ?case 
    apply(simp)
    apply(subgoal_tac "(b,B1 OR B2) ∈ set Δ'")
     apply(drule ccloses_elim)
      apply(assumption)
     apply(erule exE)+ 
     apply(simp del: NEGc.simps)
     apply(generate_fresh "coname")
     apply(fresh_fun_simp)
     apply(rule_tac B="B1 OR B2" in CUT_SNa)
      apply(simp)
      apply(rule disjI2)
      apply(rule disjI2)
      apply(rule disjI2)
      apply(rule_tac x="a" in exI)
      apply(rule_tac x="c" in exI)
      apply(rule_tac x="θ_n,θ_c<M>" in exI)
      apply(simp)
      apply(rule conjI)
       apply(rule fic.intros)
       apply(simp del: NEGc.simps add: abs_fresh fresh_prod fresh_atm)
       apply(rule psubst_fresh_coname)
         apply(simp)
        apply(simp)
       apply(simp)
      apply(rule BINDING_implies_CAND)
      apply(unfold BINDINGc_def)
      apply(simp (no_asm))
      apply(rule_tac x="a" in exI)
      apply(rule_tac x="θ_n,θ_c<M>" in exI)
      apply(simp (no_asm))
      apply(rule allI)+
      apply(rule impI)    
      apply(simp del: NEGc.simps add: psubst_csubst[symmetric])
      apply(drule_tac x="θ_n" in meta_spec)
      apply(drule_tac x="(a,xa,Pa)#θ_c" in meta_spec)
      apply(drule meta_mp)
       apply(assumption)
      apply(drule meta_mp)
       apply(rule ccloses_extend)
          apply(rule ccloses_subset)
           apply(assumption)
          apply(blast)
         apply(simp)
        apply(simp)
       apply(simp)
      apply(assumption)
     apply(simp)
    apply(blast)
    done
next
  case (TImpL a Δ N x Γ M y B C Γ' θ_n θ_c)
  then show ?case
    apply(simp)
    apply(subgoal_tac "(y,B IMP C) ∈ set Γ'")
     apply(drule ncloses_elim)
      apply(assumption)
     apply(erule exE)+
     apply(simp del: NEGc.simps)
     apply(generate_fresh "name")
     apply(fresh_fun_simp)
     apply(rule_tac B="B IMP C" in CUT_SNa)
      apply(simp)
     apply(rule NEG_intro)
     apply(simp (no_asm))
     apply(rule disjI2)
     apply(rule disjI2)
     apply(rule_tac x="x" in exI)
     apply(rule_tac x="a" in exI)
     apply(rule_tac x="ca" in exI)
     apply(rule_tac x="θ_n,θ_c<M>" in exI)
     apply(rule_tac x="θ_n,θ_c<N>" in exI)
     apply(simp del: NEGc.simps)
     apply(rule conjI)
      apply(rule fin.intros)
       apply(rule psubst_fresh_name)
         apply(simp)
        apply(simp)
       apply(simp)
      apply(simp del: NEGc.simps add: abs_fresh fresh_prod fresh_atm)
      apply(rule psubst_fresh_name)
        apply(simp)
       apply(simp)
      apply(simp)
     apply(rule conjI)
      apply(rule BINDING_implies_CAND)
      apply(unfold BINDINGc_def)
      apply(simp del: NEGc.simps)
      apply(rule_tac x="a" in exI)
      apply(rule_tac x="θ_n,θ_c<M>" in exI)
      apply(simp del: NEGc.simps)
      apply(rule allI)+
      apply(rule impI)
      apply(simp del: NEGc.simps add: psubst_csubst[symmetric])
      apply(drule_tac x="θ_n" in meta_spec)
      apply(drule_tac x="(a,xa,Pa)#θ_c" in meta_spec)
      apply(drule meta_mp)
       apply(rule ncloses_subset)
        apply(assumption)
       apply(blast)
      apply(drule meta_mp)
       apply(rule ccloses_extend)
          apply(assumption)
         apply(simp)
        apply(simp)
       apply(assumption)
      apply(assumption)
     apply(rule BINDING_implies_CAND)
     apply(unfold BINDINGn_def)
     apply(simp del: NEGc.simps)
     apply(rule_tac x="x" in exI)
     apply(rule_tac x="θ_n,θ_c<N>" in exI)
     apply(simp del: NEGc.simps)
     apply(rule allI)+
     apply(rule impI)
     apply(simp del: NEGc.simps add: psubst_nsubst[symmetric])
     apply(rotate_tac 12)
     apply(drule_tac x="(x,aa,Pa)#θ_n" in meta_spec)
     apply(drule_tac x="θ_c" in meta_spec)
     apply(drule meta_mp)
      apply(rule ncloses_extend)
         apply(rule ncloses_subset)
          apply(assumption)
         apply(blast)
        apply(simp)
       apply(simp)
      apply(assumption)
     apply(drule meta_mp)
      apply(assumption)
     apply(assumption)
    apply(blast)
    done
next
  case (TImpR a Δ b x Γ B M C Δ' θ_n θ_c)
  then show ?case
    apply(simp)
    apply(subgoal_tac "(b,B IMP C) ∈ set Δ'")
     apply(drule ccloses_elim)
      apply(assumption)
     apply(erule exE)+
     apply(simp)
     apply(generate_fresh "coname")
     apply(fresh_fun_simp)
     apply(rule_tac B="B IMP C" in CUT_SNa)
      apply(simp)
      apply(rule disjI2)
      apply(rule disjI2)
      apply(rule_tac x="x" in exI)
      apply(rule_tac x="a" in exI)
      apply(rule_tac x="c" in exI)
      apply(rule_tac x="θ_n,θ_c<M>" in exI)
      apply(simp)
      apply(rule conjI)
       apply(rule fic.intros)
       apply(simp add: abs_fresh fresh_prod fresh_atm)
       apply(rule psubst_fresh_coname)
         apply(simp)
        apply(simp)
       apply(simp)
      apply(rule conjI)
       apply(rule allI)+
       apply(rule impI)
       apply(simp add: psubst_csubst[symmetric])
       apply(rule BINDING_implies_CAND)
       apply(unfold BINDINGn_def)
       apply(simp)
       apply(rule_tac x="x" in exI)
       apply(rule_tac x="θ_n,((a,z,Pa)#θ_c)<M>" in exI)
       apply(simp)
       apply(rule allI)+
       apply(rule impI)
       apply(rule_tac t="θ_n,((a,z,Pa)#θ_c)<M>{x:=<aa>.Pb}" and 
        s="((x,aa,Pb)#θ_n),((a,z,Pa)#θ_c)<M>" in subst)
        apply(rule psubst_nsubst)
        apply(simp add: fresh_prod fresh_atm fresh_list_cons)
       apply(drule_tac x="(x,aa,Pb)#θ_n" in meta_spec)
       apply(drule_tac x="(a,z,Pa)#θ_c" in meta_spec)
       apply(drule meta_mp)
        apply(rule ncloses_extend)
           apply(assumption)
          apply(simp)
         apply(simp)
        apply(simp)
       apply(drule meta_mp)
        apply(rule ccloses_extend)
           apply(rule ccloses_subset)
            apply(assumption)
           apply(blast)
          apply(auto intro: fresh_subset simp del: NEGc.simps)[1]
         apply(simp)
        apply(simp)
       apply(assumption)
      apply(rule allI)+
      apply(rule impI)
      apply(simp add: psubst_nsubst[symmetric])
      apply(rule BINDING_implies_CAND)
      apply(unfold BINDINGc_def)
      apply(simp)
      apply(rule_tac x="a" in exI)
      apply(rule_tac x="((x,ca,Q)#θ_n),θ_c<M>" in exI)
      apply(simp)
      apply(rule allI)+
      apply(rule impI)
      apply(rule_tac t="((x,ca,Q)#θ_n),θ_c<M>{a:=(xaa).Pa}" and 
        s="((x,ca,Q)#θ_n),((a,xaa,Pa)#θ_c)<M>" in subst)
       apply(rule psubst_csubst)
       apply(simp add: fresh_prod fresh_atm fresh_list_cons)
      apply(drule_tac x="(x,ca,Q)#θ_n" in meta_spec)
      apply(drule_tac x="(a,xaa,Pa)#θ_c" in meta_spec)
      apply(drule meta_mp)
       apply(rule ncloses_extend)
          apply(assumption)
         apply(simp)
        apply(simp)
       apply(simp)
      apply(drule meta_mp)
       apply(rule ccloses_extend)
          apply(rule ccloses_subset)
           apply(assumption)
          apply(blast)
         apply(auto intro: fresh_subset simp del: NEGc.simps)[1]
        apply(simp)
       apply(simp)
      apply(assumption)
     apply(simp)
    apply(blast)
    done
next
  case (TCut a Δ N x Γ M B θ_n θ_c)
  then show ?case 
    apply -
    apply(case_tac "∀y. M≠Ax y a")
     apply(case_tac "∀c. N≠Ax x c")
      apply(simp)
      apply(rule_tac B="B" in CUT_SNa)
       apply(rule BINDING_implies_CAND)
       apply(unfold BINDINGc_def)
       apply(simp)
       apply(rule_tac x="a" in exI)
       apply(rule_tac x="θ_n,θ_c<M>" in exI)
       apply(simp)
       apply(rule allI)
       apply(rule allI)
       apply(rule impI)
       apply(simp add: psubst_csubst[symmetric]) (*?*)
       apply(drule_tac x="θ_n" in meta_spec)
       apply(drule_tac x="(a,xa,P)#θ_c" in meta_spec)
       apply(drule meta_mp)
        apply(assumption)
       apply(drule meta_mp)
        apply(rule ccloses_extend) 
           apply(assumption)
          apply(assumption)
         apply(assumption)
        apply(assumption)
       apply(assumption)
      apply(rule BINDING_implies_CAND)
      apply(unfold BINDINGn_def)
      apply(simp)
      apply(rule_tac x="x" in exI)
      apply(rule_tac x="θ_n,θ_c<N>" in exI)
      apply(simp)
      apply(rule allI)
      apply(rule allI)
      apply(rule impI)
      apply(simp add: psubst_nsubst[symmetric]) (*?*)
      apply(rotate_tac 11)
      apply(drule_tac x="(x,aa,P)#θ_n" in meta_spec)
      apply(drule_tac x="θ_c" in meta_spec)
      apply(drule meta_mp)
       apply(rule ncloses_extend)
          apply(assumption)
         apply(assumption)
        apply(assumption)
       apply(assumption)
      apply(drule_tac meta_mp)
       apply(assumption)
      apply(assumption)
      (* cases at least one axiom *)
     apply(simp (no_asm_use))
     apply(erule exE)
     apply(simp del: psubst.simps)
     apply(drule typing_Ax_elim2)
     apply(auto simp add: trm.inject)[1]
     apply(rule_tac B="B" in CUT_SNa)
      (* left term *)
      apply(rule BINDING_implies_CAND)
      apply(unfold BINDINGc_def)
      apply(simp)
      apply(rule_tac x="a" in exI)
      apply(rule_tac x="θ_n,θ_c<M>" in exI)
      apply(simp)
      apply(rule allI)+
      apply(rule impI)
      apply(drule_tac x="θ_n" in meta_spec)
      apply(drule_tac x="(a,xa,P)#θ_c" in meta_spec)
      apply(drule meta_mp)
       apply(assumption)
      apply(drule meta_mp)
       apply(rule ccloses_extend) 
          apply(assumption)
         apply(assumption)
        apply(assumption)
       apply(assumption)
      apply(simp add: psubst_csubst[symmetric]) (*?*)
      (* right term -axiom *)
     apply(drule ccloses_elim)
      apply(assumption)
     apply(erule exE)+
     apply(erule conjE)
     apply(frule_tac y="x" in lookupd_cmaps)
     apply(drule cmaps_fresh)
      apply(assumption)
     apply(simp)
     apply(subgoal_tac "(x):P[xa⊢n>x] = (xa):P")
      apply(simp)
     apply(simp add: ntrm.inject)
     apply(simp add: alpha fresh_prod fresh_atm)
     apply(rule sym)
     apply(rule nrename_swap)
     apply(simp)
      (* M is axiom *)
    apply(simp)
    apply(auto)[1]
      (* both are axioms *)
     apply(rule_tac B="B" in CUT_SNa)
      apply(drule typing_Ax_elim1)
      apply(drule ncloses_elim)
       apply(assumption)
      apply(erule exE)+
      apply(erule conjE)
      apply(frule_tac a="a" in lookupc_nmaps)
      apply(drule_tac a="a" in nmaps_fresh)
       apply(assumption)
      apply(simp)
      apply(subgoal_tac "<a>:P[c⊢c>a] = <c>:P")
       apply(simp)
      apply(simp add: ctrm.inject)
      apply(simp add: alpha fresh_prod fresh_atm)
      apply(rule sym)
      apply(rule crename_swap)
      apply(simp)
     apply(drule typing_Ax_elim2)
     apply(drule ccloses_elim)
      apply(assumption)
     apply(erule exE)+
     apply(erule conjE)
     apply(frule_tac y="x" in lookupd_cmaps)
     apply(drule cmaps_fresh)
      apply(assumption)
     apply(simp)
     apply(subgoal_tac "(x):P[xa⊢n>x] = (xa):P")
      apply(simp)
     apply(simp add: ntrm.inject)
     apply(simp add: alpha fresh_prod fresh_atm)
     apply(rule sym)
     apply(rule nrename_swap)
     apply(simp)
      (* N is not axioms *)
    apply(rule_tac B="B" in CUT_SNa)
      (* left term *)
     apply(drule typing_Ax_elim1)
     apply(drule ncloses_elim)
      apply(assumption)
     apply(erule exE)+
     apply(erule conjE)
     apply(frule_tac a="a" in lookupc_nmaps)
     apply(drule_tac a="a" in nmaps_fresh)
      apply(assumption)
     apply(simp)
     apply(subgoal_tac "<a>:P[c⊢c>a] = <c>:P")
      apply(simp)
     apply(simp add: ctrm.inject)
     apply(simp add: alpha fresh_prod fresh_atm)
     apply(rule sym)
     apply(rule crename_swap)
     apply(simp)
    apply(rule BINDING_implies_CAND)
    apply(unfold BINDINGn_def)
    apply(simp)
    apply(rule_tac x="x" in exI)
    apply(rule_tac x="θ_n,θ_c<N>" in exI)
    apply(simp)
    apply(rule allI)
    apply(rule allI)
    apply(rule impI)
    apply(simp add: psubst_nsubst[symmetric]) (*?*)
    apply(rotate_tac 10)
    apply(drule_tac x="(x,aa,P)#θ_n" in meta_spec)
    apply(drule_tac x="θ_c" in meta_spec)
    apply(drule meta_mp)
     apply(rule ncloses_extend)
        apply(assumption)
       apply(assumption)
      apply(assumption)
     apply(assumption)
    apply(drule_tac meta_mp)
     apply(assumption)
    apply(assumption)
    done
qed

primrec "idn" :: "(name×ty) list⇒coname⇒(name×coname×trm) list" where
  "idn [] a   = []"
| "idn (p#Γ) a = ((fst p),a,Ax (fst p) a)#(idn Γ a)"

primrec "idc" :: "(coname×ty) list⇒name⇒(coname×name×trm) list" where
  "idc [] x    = []"
| "idc (p#Δ) x = ((fst p),x,Ax x (fst p))#(idc Δ x)"

lemma idn_eqvt[eqvt]:
  fixes pi1::"name prm"
    and   pi2::"coname prm"
  shows "(pi1∙(idn Γ a)) = idn (pi1∙Γ) (pi1∙a)"
    and   "(pi2∙(idn Γ a)) = idn (pi2∙Γ) (pi2∙a)"
   apply(induct Γ)
     apply(auto)
  done

lemma idc_eqvt[eqvt]:
  fixes pi1::"name prm"
    and   pi2::"coname prm"
  shows "(pi1∙(idc Δ x)) = idc (pi1∙Δ) (pi1∙x)"
    and   "(pi2∙(idc Δ x)) = idc (pi2∙Δ) (pi2∙x)"
   apply(induct Δ)
     apply(auto)
  done

lemma ccloses_id:
  shows "(idc Δ x) ccloses Δ"
  apply(induct Δ)
   apply(auto simp add: ccloses_def)
   apply(rule Ax_in_CANDs)
  apply(rule Ax_in_CANDs)
  done

lemma ncloses_id:
  shows "(idn Γ a) ncloses Γ"
  apply(induct Γ)
   apply(auto simp add: ncloses_def)
   apply(rule Ax_in_CANDs)
  apply(rule Ax_in_CANDs)
  done

lemma fresh_idn:
  fixes x::"name"
    and   a::"coname"
  shows "x♯Γ ⟹ x♯idn Γ a"
    and   "a♯(Γ,b) ⟹ a♯idn Γ b"
   apply(induct Γ)
     apply(auto simp add: fresh_list_cons fresh_list_nil fresh_atm fresh_prod)
  done

lemma fresh_idc:
  fixes x::"name"
    and   a::"coname"
  shows "x♯(Δ,y) ⟹ x♯idc Δ y"
    and   "a♯Δ  ⟹ a♯idc Δ y"
   apply(induct Δ)
     apply(auto simp add: fresh_list_cons fresh_list_nil fresh_atm fresh_prod)
  done

lemma idc_cmaps:
  assumes a: "idc Δ y cmaps b to Some (x,M)"
  shows "M=Ax x b"
  using a
  apply(induct Δ)
   apply(auto)
  apply(case_tac "b=a")
   apply(auto)
  done

lemma idn_nmaps:
  assumes a: "idn Γ a nmaps x to Some (b,M)"
  shows "M=Ax x b"
  using a
  apply(induct Γ)
   apply(auto)
  apply(case_tac "aa=x")
   apply(auto)
  done

lemma lookup1:
  assumes a: "x♯(idn Γ b)"
  shows "lookup x a (idn Γ b) θ_c = lookupa x a θ_c"
  using a
  apply(induct Γ)
   apply(auto simp add: fresh_list_cons fresh_prod fresh_atm)
  done

lemma lookup2:
  assumes a: "¬(x♯(idn Γ b))"
  shows "lookup x a (idn Γ b) θ_c = lookupb x a θ_c b (Ax x b)"
  using a
  apply(induct Γ)
   apply(auto simp add: fresh_list_cons fresh_prod fresh_atm fresh_list_nil)
  done

lemma lookup3:
  assumes a: "a♯(idc Δ y)"
  shows "lookupa x a (idc Δ y) = Ax x a"
  using a
  apply(induct Δ)
   apply(auto simp add: fresh_list_cons fresh_prod fresh_atm)
  done

lemma lookup4:
  assumes a: "¬(a♯(idc Δ y))"
  shows "lookupa x a (idc Δ y) = Cut <a>.(Ax x a) (y).Ax y a"
  using a
  apply(induct Δ)
   apply(auto simp add: fresh_list_cons fresh_prod fresh_atm fresh_list_nil)
  done

lemma lookup5:
  assumes a: "a♯(idc Δ y)"
  shows "lookupb x a (idc Δ y) c P = Cut <c>.P (x).Ax x a"
  using a
  apply(induct Δ)
   apply(auto simp add: fresh_list_cons fresh_prod fresh_atm fresh_list_nil)
  done

lemma lookup6:
  assumes a: "¬(a♯(idc Δ y))"
  shows "lookupb x a (idc Δ y) c P = Cut <c>.P (y).Ax y a"
  using a
  apply(induct Δ)
   apply(auto simp add: fresh_list_cons fresh_prod fresh_atm fresh_list_nil)
  done

lemma lookup7:
  shows "lookupc x a (idn Γ b) = Ax x a"
  apply(induct Γ)
   apply(auto simp add: fresh_list_cons fresh_prod fresh_atm fresh_list_nil)
  done

lemma lookup8:
  shows "lookupd x a (idc Δ y) = Ax x a"
  apply(induct Δ)
   apply(auto simp add: fresh_list_cons fresh_prod fresh_atm fresh_list_nil)
  done

lemma id_redu:
  shows "(idn Γ x),(idc Δ a)<M> ⟶⇩a* M"
  apply(nominal_induct M avoiding: Γ Δ x a rule: trm.strong_induct)
             apply(auto)
    (* Ax *)
             apply(case_tac "name♯(idn Γ x)")
              apply(simp add: lookup1)
              apply(case_tac "coname♯(idc Δ a)")
               apply(simp add: lookup3)
              apply(simp add: lookup4)
              apply(rule rtranclp_trans)
               apply(rule a_starI)
               apply(rule al_redu)
               apply(rule better_LAxR_intro)
               apply(rule fic.intros)
              apply(simp)
             apply(simp add: lookup2)
             apply(case_tac "coname♯(idc Δ a)")
              apply(simp add: lookup5)
              apply(rule rtranclp_trans)
               apply(rule a_starI)
               apply(rule al_redu)
               apply(rule better_LAxR_intro)
               apply(rule fic.intros)
              apply(simp)
             apply(simp add: lookup6)
             apply(rule rtranclp_trans)
              apply(rule a_starI)
              apply(rule al_redu)
              apply(rule better_LAxR_intro)
              apply(rule fic.intros)
             apply(simp)
    (* Cut *)
            apply(auto simp add: fresh_idn fresh_idc psubst_fresh_name psubst_fresh_coname fresh_atm fresh_prod )[1]
               apply(simp add: lookup7 lookup8)
              apply(simp add: lookup7 lookup8)
              apply(simp add: a_star_Cut)
             apply(simp add: lookup7 lookup8)
             apply(simp add: a_star_Cut)
            apply(simp add: a_star_Cut)
    (* NotR *)
           apply(simp add: fresh_idn fresh_idc)
           apply(case_tac "findc (idc Δ a) coname")
            apply(simp)
            apply(simp add: a_star_NotR)
           apply(auto)[1]
           apply(generate_fresh "coname")
           apply(fresh_fun_simp)
           apply(drule idc_cmaps)
           apply(simp)
           apply(subgoal_tac "c♯idn Γ x,idc Δ a<trm>")
            apply(rule rtranclp_trans)
             apply(rule a_starI)
             apply(rule al_redu)
             apply(rule better_LAxR_intro)
             apply(rule fic.intros)
             apply(assumption)
            apply(simp add: crename_fresh)
            apply(simp add: a_star_NotR)
           apply(rule psubst_fresh_coname)
             apply(rule fresh_idn)
             apply(simp)
            apply(rule fresh_idc)
            apply(simp)
           apply(simp)
    (* NotL *)
          apply(simp add: fresh_idn fresh_idc)
          apply(case_tac "findn (idn Γ x) name")
           apply(simp)
           apply(simp add: a_star_NotL)
          apply(auto)[1]
          apply(generate_fresh "name")
          apply(fresh_fun_simp)
          apply(drule idn_nmaps)
          apply(simp)
          apply(subgoal_tac "c♯idn Γ x,idc Δ a<trm>")
           apply(rule rtranclp_trans)
            apply(rule a_starI)
            apply(rule al_redu)
            apply(rule better_LAxL_intro)
            apply(rule fin.intros)
            apply(assumption)
           apply(simp add: nrename_fresh)
           apply(simp add: a_star_NotL)
          apply(rule psubst_fresh_name)
            apply(rule fresh_idn)
            apply(simp)
           apply(rule fresh_idc)
           apply(simp)
          apply(simp)
    (* AndR *)
         apply(simp add: fresh_idn fresh_idc)
         apply(case_tac "findc (idc Δ a) coname3")
          apply(simp)
          apply(simp add: a_star_AndR)
         apply(auto)[1]
         apply(generate_fresh "coname")
         apply(fresh_fun_simp)
         apply(drule idc_cmaps)
         apply(simp)
         apply(subgoal_tac "c♯idn Γ x,idc Δ a<trm1>")
          apply(subgoal_tac "c♯idn Γ x,idc Δ a<trm2>")
           apply(rule rtranclp_trans)
            apply(rule a_starI)
            apply(rule al_redu)
            apply(rule better_LAxR_intro)
            apply(rule fic.intros)
             apply(simp add: abs_fresh)
            apply(simp add: abs_fresh)
           apply(auto simp add: fresh_idn fresh_idc psubst_fresh_name crename_fresh fresh_atm fresh_prod )[1]
           apply(rule aux3)
            apply(rule crename.simps)
              apply(auto simp add: fresh_prod fresh_atm)[1]
              apply(rule psubst_fresh_coname)
                apply(rule fresh_idn)
                apply(simp add: fresh_prod fresh_atm)
               apply(rule fresh_idc)
               apply(simp)
              apply(simp)
             apply(auto simp add: fresh_prod fresh_atm)[1]
             apply(rule psubst_fresh_coname)
               apply(rule fresh_idn)
               apply(simp add: fresh_prod fresh_atm)
              apply(rule fresh_idc)
              apply(simp)
             apply(simp)
            apply(simp)
           apply(simp)
           apply(simp add: crename_fresh)
           apply(simp add: a_star_AndR)
          apply(rule psubst_fresh_coname)
            apply(rule fresh_idn)
            apply(simp)
           apply(rule fresh_idc)
           apply(simp)
          apply(simp)
         apply(rule psubst_fresh_coname)
           apply(rule fresh_idn)
           apply(simp)
          apply(rule fresh_idc)
          apply(simp)
         apply(simp)
    (* AndL1 *)
        apply(simp add: fresh_idn fresh_idc)
        apply(case_tac "findn (idn Γ x) name2")
         apply(simp)
         apply(simp add: a_star_AndL1)
        apply(auto)[1]
        apply(generate_fresh "name")
        apply(fresh_fun_simp)
        apply(drule idn_nmaps)
        apply(simp)
        apply(subgoal_tac "c♯idn Γ x,idc Δ a<trm>")
         apply(rule rtranclp_trans)
          apply(rule a_starI)
          apply(rule al_redu)
          apply(rule better_LAxL_intro)
          apply(rule fin.intros)
          apply(simp add: abs_fresh)
         apply(rule aux3)
          apply(rule nrename.simps)
          apply(auto simp add: fresh_prod fresh_atm)[1]
         apply(simp)
         apply(simp add: nrename_fresh)
         apply(simp add: a_star_AndL1)
        apply(rule psubst_fresh_name)
          apply(rule fresh_idn)
          apply(simp)
         apply(rule fresh_idc)
         apply(simp)
        apply(simp)
    (* AndL2 *)
       apply(simp add: fresh_idn fresh_idc)
       apply(case_tac "findn (idn Γ x) name2")
        apply(simp)
        apply(simp add: a_star_AndL2)
       apply(auto)[1]
       apply(generate_fresh "name")
       apply(fresh_fun_simp)
       apply(drule idn_nmaps)
       apply(simp)
       apply(subgoal_tac "c♯idn Γ x,idc Δ a<trm>")
        apply(rule rtranclp_trans)
         apply(rule a_starI)
         apply(rule al_redu)
         apply(rule better_LAxL_intro)
         apply(rule fin.intros)
         apply(simp add: abs_fresh)
        apply(rule aux3)
         apply(rule nrename.simps)
         apply(auto simp add: fresh_prod fresh_atm)[1]
        apply(simp)
        apply(simp add: nrename_fresh)
        apply(simp add: a_star_AndL2)
       apply(rule psubst_fresh_name)
         apply(rule fresh_idn)
         apply(simp)
        apply(rule fresh_idc)
        apply(simp)
       apply(simp)
    (* OrR1 *)
      apply(simp add: fresh_idn fresh_idc)
      apply(case_tac "findc (idc Δ a) coname2")
       apply(simp)
       apply(simp add: a_star_OrR1)
      apply(auto)[1]
      apply(generate_fresh "coname")
      apply(fresh_fun_simp)
      apply(drule idc_cmaps)
      apply(simp)
      apply(subgoal_tac "c♯idn Γ x,idc Δ a<trm>")
       apply(rule rtranclp_trans)
        apply(rule a_starI)
        apply(rule al_redu)
        apply(rule better_LAxR_intro)
        apply(rule fic.intros)
        apply(simp add: abs_fresh)
       apply(rule aux3)
        apply(rule crename.simps)
        apply(auto simp add: fresh_prod fresh_atm)[1]
       apply(simp)
       apply(simp add: crename_fresh)
       apply(simp add: a_star_OrR1)
      apply(rule psubst_fresh_coname)
        apply(rule fresh_idn)
        apply(simp)
       apply(rule fresh_idc)
       apply(simp)
      apply(simp)
    (* OrR2 *)
     apply(simp add: fresh_idn fresh_idc)
     apply(case_tac "findc (idc Δ a) coname2")
      apply(simp)
      apply(simp add: a_star_OrR2)
     apply(auto)[1]
     apply(generate_fresh "coname")
     apply(fresh_fun_simp)
     apply(drule idc_cmaps)
     apply(simp)
     apply(subgoal_tac "c♯idn Γ x,idc Δ a<trm>")
      apply(rule rtranclp_trans)
       apply(rule a_starI)
       apply(rule al_redu)
       apply(rule better_LAxR_intro)
       apply(rule fic.intros)
       apply(simp add: abs_fresh)
      apply(rule aux3)
       apply(rule crename.simps)
       apply(auto simp add: fresh_prod fresh_atm)[1]
      apply(simp)
      apply(simp add: crename_fresh)
      apply(simp add: a_star_OrR2)
     apply(rule psubst_fresh_coname)
       apply(rule fresh_idn)
       apply(simp)
      apply(rule fresh_idc)
      apply(simp)
     apply(simp)
    (* OrL *)
    apply(simp add: fresh_idn fresh_idc)
    apply(case_tac "findn (idn Γ x) name3")
     apply(simp)
     apply(simp add: a_star_OrL)
    apply(auto)[1]
    apply(generate_fresh "name")
    apply(fresh_fun_simp)
    apply(drule idn_nmaps)
    apply(simp)
    apply(subgoal_tac "c♯idn Γ x,idc Δ a<trm1>")
     apply(subgoal_tac "c♯idn Γ x,idc Δ a<trm2>")
      apply(rule rtranclp_trans)
       apply(rule a_starI)
       apply(rule al_redu)
       apply(rule better_LAxL_intro)
       apply(rule fin.intros)
        apply(simp add: abs_fresh)
       apply(simp add: abs_fresh)
      apply(rule aux3)
       apply(rule nrename.simps)
         apply(auto simp add: fresh_prod fresh_atm)[1]
         apply(rule psubst_fresh_name)
           apply(rule fresh_idn)
           apply(simp)
          apply(rule fresh_idc)
          apply(simp add: fresh_prod fresh_atm)
         apply(simp)
        apply(auto simp add: fresh_prod fresh_atm)[1]
        apply(rule psubst_fresh_name)
          apply(rule fresh_idn)
          apply(simp)
         apply(rule fresh_idc)
         apply(simp add: fresh_prod fresh_atm)
        apply(simp)
       apply(simp)
      apply(simp)
      apply(simp add: nrename_fresh)
      apply(simp add: a_star_OrL)
     apply(rule psubst_fresh_name)
       apply(rule fresh_idn)
       apply(simp)
      apply(rule fresh_idc)
      apply(simp)
     apply(simp)
    apply(rule psubst_fresh_name)
      apply(rule fresh_idn)
      apply(simp)
     apply(rule fresh_idc)
     apply(simp)
    apply(simp)
    (* ImpR *)
   apply(simp add: fresh_idn fresh_idc)
   apply(case_tac "findc (idc Δ a) coname2")
    apply(simp)
    apply(simp add: a_star_ImpR)
   apply(auto)[1]
   apply(generate_fresh "coname")
   apply(fresh_fun_simp)
   apply(drule idc_cmaps)
   apply(simp)
   apply(subgoal_tac "c♯idn Γ x,idc Δ a<trm>")
    apply(rule rtranclp_trans)
     apply(rule a_starI)
     apply(rule al_redu)
     apply(rule better_LAxR_intro)
     apply(rule fic.intros)
     apply(simp add: abs_fresh)
    apply(rule aux3)
     apply(rule crename.simps)
     apply(auto simp add: fresh_prod fresh_atm)[1]
    apply(simp)
    apply(simp add: crename_fresh)
    apply(simp add: a_star_ImpR)
   apply(rule psubst_fresh_coname)
     apply(rule fresh_idn)
     apply(simp)
    apply(rule fresh_idc)
    apply(simp)
   apply(simp)
    (* ImpL *)
  apply(simp add: fresh_idn fresh_idc)
  apply(case_tac "findn (idn Γ x) name2")
   apply(simp)
   apply(simp add: a_star_ImpL)
  apply(auto)[1]
  apply(generate_fresh "name")
  apply(fresh_fun_simp)
  apply(drule idn_nmaps)
  apply(simp)
  apply(subgoal_tac "c♯idn Γ x,idc Δ a<trm1>")
   apply(subgoal_tac "c♯idn Γ x,idc Δ a<trm2>")
    apply(rule rtranclp_trans)
     apply(rule a_starI)
     apply(rule al_redu)
     apply(rule better_LAxL_intro)
     apply(rule fin.intros)
      apply(simp add: abs_fresh)
     apply(simp add: abs_fresh)
    apply(rule aux3)
     apply(rule nrename.simps)
      apply(auto simp add: fresh_prod fresh_atm)[1]
      apply(rule psubst_fresh_coname)
        apply(rule fresh_idn)
        apply(simp add: fresh_atm)
       apply(rule fresh_idc)
       apply(simp add: fresh_prod fresh_atm)
      apply(simp)
     apply(auto simp add: fresh_prod fresh_atm)[1]
     apply(rule psubst_fresh_name)
       apply(rule fresh_idn)
       apply(simp)
      apply(rule fresh_idc)
      apply(simp add: fresh_prod fresh_atm)
     apply(simp)
    apply(simp)
    apply(simp add: nrename_fresh)
    apply(simp add: a_star_ImpL)
   apply(rule psubst_fresh_name)
     apply(rule fresh_idn)
     apply(simp)
    apply(rule fresh_idc)
    apply(simp)
   apply(simp)
  apply(rule psubst_fresh_name)
    apply(rule fresh_idn)
    apply(simp)
   apply(rule fresh_idc)
   apply(simp)
  apply(simp)
  done

theorem ALL_SNa:
  assumes a: "Γ ⊢ M ⊢ Δ"
  shows "SNa M"
proof -
  fix x have "(idc Δ x) ccloses Δ" by (simp add: ccloses_id)
  moreover
  fix a have "(idn Γ a) ncloses Γ" by (simp add: ncloses_id)
  ultimately have "SNa ((idn Γ a),(idc Δ x)<M>)" using a by (simp add: all_CAND)
  moreover
  have "((idn Γ a),(idc Δ x)<M>) ⟶⇩a* M" by (simp add: id_redu)
  ultimately show "SNa M" by (simp add: a_star_preserves_SNa)
qed

end