proposition: Lemma continuation_subrelation o o' (cont: o ≼ o'): subrelation (o.R) (o'.R).
proof: Proof. destruct cont as [sub cont coincide]. intros x y rel. destruct (o.good) as [_ _ _ _ correct _]. apply coincide; trivial; apply correct in rel; tauto. Qed.
imports: Coq(Relations Equivalence Morphisms Utf8) Coq(ChoiceFacts ClassicalFacts) Coq.Program(Basics) Coq.Logic(SetoidChoice)