lemma ac_top_props: ac_props ac_top ≝ mk_ac_props ….
/3 width=3 by or_introl, ex2_intro/
qed.
definition ac_eq (k): ac ≝ mk_ac (eq … k).
lemma ac_top_props: ac_props ac_top ≝ mk_ac_props ….
/3 width=3 by or_introl, ex2_intro/
qed.
definition ac_eq (k): ac ≝ mk_ac (eq … k).