fact: Hypothesis simulation: forall c1 c1', step1 c1 c1' -> forall c2, inv c1 c2 -> exists c2', (plus step2 c2 c2' \/ (star step2 c2 c2' /\ measure c1' < measure c1)) /\ inv c1' c2'.
imports: Coq(Psatz) CDF(Sequences)