proposition: Lemma alwas_sc_mtac2 : forall p, steps p ;;.
proof: Proof. MProof. intros p. (select st >>= induction) &> case steps0 do eauto [x]. (select exp >>= induction) &> case false, nil do eauto [x]. + stepIfTrue. + (select binop >>= destruct) &> (select exp >>= induction) &> eauto [x]. + (select unop >>= destruct) &> (select exp >>= induction) &> case true, B, U do eauto [x] &> (stepInIf &> stepIfTrue). Qed.
imports: Mtac2(Mtac2 ConstrSelector)