proposition: Lemma elements_extensional: forall (A: Type) (m n: ptrie A) o, wf o m -> wf o n -> (forall i, get' i m = get' i n) -> elements' m = elements' n.
proof: Proof. intros. generalize (ptrie_extensional H H0 H1). intro; subst; auto. Qed.
imports: Lia Cdcl.Coqlib