proposition: Lemma hdisjoint_sym: forall h1 h2, hdisjoint h1 h2 -> hdisjoint h2 h1.
proof: Proof. unfold hdisjoint; intros. specialize (H l); tauto. Qed.
imports: Coq(ZArith Psatz Bool String List Wellfounded Program.Equality) Coq(FunctionalExtensionality PropExtensionality) CDF(IMP Sequences)