proposition: Lemma always_sc : forall p, steps p ;;.
proof: Proof. induction 0; eauto. induction e; eauto. - eapply stepsn; repeat (assumption || econstructor || discriminate). - case b; induction e1; eauto. - case u; induction e; eauto. + eapply stepsn. eapply Ife. econstructor. simpl. eapply stepsn. eapply IfT. econstructor. discriminate. discriminate. assumption. + eapply stepsn. eapply Ife. econstructor. simpl. eapply stepsn. eapply IfT. econstructor. discriminate. discriminate. assumption. Qed.