36   shows "x \<approx> x"

    36   shows "x \<approx> x"

    37   apply (rule rlam.induct)

    37   apply (rule rlam.induct)

    38   apply (simp_all add:a1 a2)

    38   apply (simp_all add:a1 a2)

    39   apply (rule a3)

    39   apply (rule a3)

    40   apply (simp_all)

    40   apply (simp_all)

    41 sorry

    42 sorry

    42 

    43 

    43 quotient lam = rlam / alpha

    44 quotient lam = rlam / alpha

    44 sorry

    45 sorry

    45 

    46