proposition: Lemma insert_eq_insert_3: forall A x1 x2 a1 a2 (e1 e2 : env A), insert x1 a1 e1 = insert x2 a2 e2 -> x1 <> x2 -> exists e y1 y2, e1 = insert y1 a2 e /\ e2 = insert y2 a1 e /\ shift x1 y1 = x2 /\ y2 = (if le_gt_dec x1 y1 then x1 else x1 - 1).
proof: Proof. induction x1; intros. destruct x2; [ omega | ]. rewrite raw_insert_zero in *. rewrite raw_insert_successor in *. match goal with h: _ = _ |- _ => injection h; clear h; intros end. destruct e2; [ congruence | ]. subst. simpl. exists e2. exists x2. exists 0. eauto. destruct x2. rewrite raw_insert_zero in *. rewrite raw_insert_successor in *. match goal with h: _ = _ |- _ => injection h; clear h; intros end. destruct e1; [ congruence | ]. subst. exists e1. exists 0. exists x1. split. eauto. split. eauto. split. eauto. dblib_by_cases. omega. do 2 rewrite raw_insert_successor in *. assert (xx: x1 <> x2). omega. match goal with h: _ = _ |- _ => injection h; clear h; intros h ?; generalize (IHx1 _ _ _ _ _ h xx); intros [ e [ y1 [ y2 [ ? [ ? [ ? ? ]]]]]] end. destruct e1; simpl tl in *; [ elimtype False; eauto using insert_nil | ]. destruct e2; simpl tl in *; [ elimtype False; eauto using insert_nil | ]. exists (o :: e). exists (S y1). exists (S y2). split. simpl. congruence. split. simpl. congruence. split. eapply translate_lift with (k := 1). eauto. dblib_by_cases; omega. Qed.
imports: List Dblib(DblibTactics DeBruijn)