proposition: Lemma subsume_insert_inversion: forall e1 x a2 e2, subsume e1 (insert x a2 e2) -> exists f1 a1, e1 = insert x a1 f1 /\ subsume f1 e2 /\ sub a1 a2.
proof: Proof. induction e1; simpl; intros. - elimtype False. match goal with h: subsume nil _ |- _ => generalize (h x); clear h; intro h; rewrite lookup_insert_bingo in h by reflexivity; rewrite lookup_empty_None in h end. solve [ eauto using osub_None_Some ]. - { destruct x. - match goal with h: subsume _ _ |- _ => rewrite raw_insert_zero in h; generalize (subsume_cons_cons_inversion h); clear h; intros [ h ? ]; generalize (osub_Some_inversion h); intros [ ? [ ? ? ]]; subst end. do 2 eexists. rewrite raw_insert_zero. solve [ eauto ]. - match goal with h: subsume _ _ |- _ => rewrite raw_insert_successor in h; generalize (subsume_cons_cons_inversion h); clear h; intros [ ? h ]; generalize (IHe1 _ _ _ h); clear IHe1; intros [ f1 [ a1 [ ? [ ? ? ]]]]; subst end. exists (a :: f1). exists a1. rewrite raw_insert_successor. simpl. split; [ | split ]. reflexivity. eauto using subsume_cons. eauto. } Qed.
imports: List Arith Lia Dblib(DblibTactics DeBruijn)