proposition: Lemma subsume_insert: forall e1 e2, subsume e1 e2 -> forall x o1 o2, osub o1 o2 -> subsume (raw_insert x o1 e1) (raw_insert x o2 e2).
proof: Proof. unfold subsume. do 7 intro. intros n. case (le_gt_dec x n); [ case (eq_nat_dec x n) | ]; intros; repeat lookup_insert; eauto. Qed.
imports: List Dblib(DblibTactics DeBruijn)