39 | "height (App t1 t2) = max (height t1) (height t2) + 1"

    39 | "height (App t1 t2) = max (height t1) (height t2) + 1"

    40 | "height (Lam [x].t) = height t + 1"

    40 | "height (Lam [x].t) = height t + 1"

    41 apply(simp add: eqvt_def height_graph_def)

    41 apply(simp add: eqvt_def height_graph_def)

    42 apply(rule TrueI)

    42 apply(rule TrueI)

    43 apply(rule_tac y="x" in lam.exhaust)

    43 apply(rule_tac y="x" in lam.exhaust)

    44 apply(auto)

    45 apply(auto)

    45 apply(erule_tac c="()" in Abs_lst1_fcb2)

    46 apply(erule_tac c="()" in Abs_lst1_fcb2)

    46 apply(simp_all add: fresh_def pure_supp eqvt_at_def fresh_star_def)

    47 apply(simp_all add: fresh_def pure_supp eqvt_at_def fresh_star_def)

    47 done

    48 done

    48 

    49 

    59 | "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])"

    60 | "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])"

    60 | "atom x \<sharp> (y, s) \<Longrightarrow> (Lam [x]. t)[y ::= s] = Lam [x].(t[y ::= s])"

    61 | "atom x \<sharp> (y, s) \<Longrightarrow> (Lam [x]. t)[y ::= s] = Lam [x].(t[y ::= s])"

    61   unfolding eqvt_def subst_graph_def

    62   unfolding eqvt_def subst_graph_def

    62   apply(rule, perm_simp, rule)

    63   apply(rule, perm_simp, rule)

    63   apply(rule TrueI)

    64   apply(rule TrueI)

    64   apply(auto)

    66   apply(auto)

    65   apply(rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust)

    67   apply(rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust)

    66   apply(blast)+

    68   apply(blast)+

    67   apply(simp_all add: fresh_star_def fresh_Pair_elim)

    69   apply(simp_all add: fresh_star_def fresh_Pair_elim)

    68   apply(erule_tac c="(ya,sa)" in Abs_lst1_fcb2)

    70   apply(erule_tac c="(ya,sa)" in Abs_lst1_fcb2)