proposition: Lemma InDGTree_Correct: forall tree dg, InDG dg tree <-> InDGTree dg tree = true.
proof: Proof. split;intros. induction H. subst. simpl. case_eq (LocDec.eq_dec dg dg); intro; trivial. elim n; trivial. unfold InDGTree. rewrite H. destruct LocDec.eq_dec; trivial. fold InDGTree. apply fold_right_orb. exists tree'. tauto. generalize dg H. clear dg H. elim tree using DGTree_ind2 with (Q := fun kids => forall dg tree', In tree' kids -> InDGTree dg tree' = true -> InDG dg tree'). intros. unfold InDGTree in H0. case_eq (LocDec.eq_dec dg a). intros. apply InDG_base with l. unfold LocDec.eq in e. rewrite e. trivial. intros. unfold LocDec.eq in n. rewrite H1 in H0. apply fold_right_orb in H0. destruct H0 as (tree', H0). destruct H0. apply InDG_step with l a tree'; trivial. apply H; trivial. intros. inversion H. intros. simpl in H1. destruct H1. rewrite <- H1. rewrite <- H1 in H2. apply H; trivial. apply H0; trivial. Qed.
imports: Coq(List) JML(Stack) Coq(ListSet) Coq(Bool) Coq(ZArith) Coq(Relation_Operators) JML(ListHelpers) Coq(Classical) Coq(DecidableType) Coq(FSetInterface) Coq(FSetProperties) Coq(FSetEqProperties) Coq(FSetFacts) Coq(Sumbool) Coq(Lia)