proposition: Lemma agree_mon: forall L L' s1 s2, agree L' s1 s2 -> IdentSet.Subset L L' -> agree L s1 s2.
proof: Proof. unfold IdentSet.Subset, agree; intros. auto. Qed.
imports: Coq(ZArith Psatz Bool String Program.Equality FSets Wellfounded) CDF(Sequences IMP Simulation)