proposition: Lemma subsume_cons: forall o e1 e2, osub o (lookup 0 e2) -> subsume e1 (tl e2) -> subsume (o :: e1) e2.
proof: Proof. do 3 intro. intros h1 h2. intro n. destruct n. eauto. do 2 rewrite lookup_successor. eauto. Qed.
imports: List Dblib(DblibTactics DeBruijn)