proposition: Lemma steps_snoc: forall j a, steps i j -> In a (vars A) -> steps i (M A j a).
proof: Proof. setoid_rewrite bmx_str_clot. intros. eapply clot_snoc. eassumption. setoid_rewrite is_true_sup. eexists. split. eassumption. apply eqb_refl. Qed.
imports: comparisons positives ordinal pair lset monoid boolean prop sups bmx