proposition: Theorem project_In : forall hyps F g, In g hyps F -> interp_ctx hyps F [[g]].
proof: Proof. induction F;simpl. - contradiction. - intros g H;destruct H. + subst;apply compose0;simpl;trivial. + apply compose1 with [[g]];auto. Qed.
imports: List Bintree Bool BinPos