proposition: Lemma tree1_in_graph1: tree_in_graph graph1 tree1 p3.
proof: Proof. eapply TIG_T; [repeat ((left; reflexivity) || right)| | ]. eapply TIG_T; [repeat ((left; reflexivity) || right)| | ]. apply TIG_E. apply TIG_E. eapply TIG_T; [repeat ((left; reflexivity) || right)| | ]. eapply TIG_T; [repeat ((left; reflexivity) || right)| | ]. apply TIG_E. apply TIG_E. eapply TIG_T; [repeat ((left; reflexivity) || right)| | ]. apply TIG_E. apply TIG_E. Qed.
imports: VST.floyd.proofauto VST.msl.iter_sepcon Demo.treeread