proposition: Lemma osub_None_Some: forall a2, osub None (Some a2) -> False.
proof: Proof. unfold osub. intros ? h. generalize (h _ eq_refl). clear h. intros [ a1 [ ? ? ]]. congruence. Qed.
imports: List Dblib(DblibTactics DeBruijn)