proposition: Lemma subsume_cons_cons_inversion: forall o1 o2 e1 e2, subsume (o1 :: e1) (o2 :: e2) -> osub o1 o2 /\ subsume e1 e2.
proof: Proof. do 4 intro. intro h. split. eapply (h 0). intro n. eapply (h (1 + n)). Qed.
imports: List Dblib(DblibTactics DeBruijn)