proposition: Lemma assertion_extensionality: forall (P Q: assertion), (forall s h, P s h <-> Q s h) -> P = Q.
proof: Proof. intros. apply functional_extensionality; intros s. apply functional_extensionality; intros h. apply propositional_extensionality. auto. Qed.
imports: Coq(ZArith Psatz Bool String List Wellfounded Program.Equality) Coq(FunctionalExtensionality PropExtensionality) CDF(IMP Sequences)