proposition: Lemma NoDup_Subsequence: forall A (l1 l2 : list A), Subsequence l1 l2 -> NoDup l2 -> NoDup l1.
proof: Proof. intros ? ? ? ?. induction H; intros. * constructor. * constructor. inversion H0. subst x0 l. intro. apply H3. eapply Subsequence_In; eauto. apply IHSubsequence. inversion H0. trivial. * inversion H0; auto. Qed.
imports: RelationClasses VST.floyd.proofauto CertiGraph.lib.List_ext CertiGraph.binheap.binary_heap_pro CertiGraph.binheap.binary_heap_malloc_spec CertiGraph.binheap.binary_heap_model CertiGraph.binheap.binary_heap_Zmodel