15   a1: "a = b \<Longrightarrow> (rVar a) \<approx> (rVar b)"

    15   a1: "a = b \<Longrightarrow> (rVar a) \<approx> (rVar b)"

    16 | a2: "\<lbrakk>t1 \<approx> t2; s1 \<approx> s2\<rbrakk> \<Longrightarrow> rApp t1 s1 \<approx> rApp t2 s2"

    16 | a2: "\<lbrakk>t1 \<approx> t2; s1 \<approx> s2\<rbrakk> \<Longrightarrow> rApp t1 s1 \<approx> rApp t2 s2"

    17 | a3: "\<lbrakk>t \<approx> ([(a,b)]\<bullet>s); a\<sharp>[b].s\<rbrakk> \<Longrightarrow> rLam a t \<approx> rLam b s"

    17 | a3: "\<lbrakk>t \<approx> ([(a,b)]\<bullet>s); a\<sharp>[b].s\<rbrakk> \<Longrightarrow> rLam a t \<approx> rLam b s"

    18 

    18 

    19 quotient lam = rlam / alpha

    19 quotient lam = rlam / alpha

    21 sorry

    20 sorry

    22 

    21 

    23 print_quotients

    22 print_quotients

    24 

    23 

    25 quotient_def (for lam)

    24 quotient_def (for lam)