proposition: Lemma hde_bool_correct_aux : forall x y, hde D x y <-> Graph hde_bool x y.
proof: Proof. intros x y. unfold hde, hde_bool, hd_eq, Graph; simpl. pose proof (fun s x y => proj1 (@beq_symb_ok s x y)). pose proof (fun s x y => proj2 (@beq_symb_ok s x y)). rewrite <- !mem_ok. destruct (rhs x); bool; intuition auto with core; repeat match goal with | H : _ && _ = true |- _ => apply andb_elim in H; case H as [] | H : _ = true |- _ => rewrite H; cbn [andb] | H : match ?x in term _ return _ with _ => _ end |- _ => case x eqn:? in *; subst | H : match ?x in term _ return _ with _ => _ end = true |- _ => case x eqn:? in *; subst end; auto. Qed.
imports: CoLoR(ADecomp ADuplicateSymb ATrs ListUtil RelSub RelUtil AGraph LogicUtil BoolUtil AShift EqUtil ListDec)