proposition: Lemma weaken : forall hyps F f G, (interp_ctx hyps F G) -> (interp_ctx (hyps\f) (F_push f hyps F) G).
proof: Proof. induction F;simpl;intros;auto. apply compose1 with ([[a]]-> G);auto. Qed.
imports: List Bintree Bool BinPos