proposition: Lemma osub_Some_inversion: forall o1 a2, osub o1 (Some a2) -> exists a1, o1 = Some a1 /\ sub a1 a2.
proof: Proof. intros. destruct o1. - eauto. - elimtype False. eauto using osub_None_Some. Qed.
imports: List Arith Lia Dblib(DblibTactics DeBruijn)