proposition: Lemma live_upper_bound: forall c L, IdentSet.Subset (live c L) (IdentSet.union (fv_com c) L).
proof: Proof. induction c; intros; simpl. - fsetdec. - destruct (IdentSet.mem x L) eqn:MEM; fsetdec. - specialize (IHc1 (live c2 L)). specialize (IHc2 L). fsetdec. - specialize (IHc1 L). specialize (IHc2 L). fsetdec. - apply postfixpoint_upper_bound. intros x. specialize (IHc x). fsetdec. Qed.
imports: Coq(ZArith Psatz Bool String Program.Equality FSets Wellfounded) CDF(Sequences IMP Simulation)