proposition: Lemma rev_aux_app_hetero : forall (A : Set) (i j1 j2 : nat) (l : ilist A i) (acc1 : ilist A j1) (acc2 : ilist A j2), (_, irev_aux l (iapp acc1 acc2)) = (_, iapp (irev_aux l acc1) acc2).
proof: Proof. intros. funelim (irev_aux l acc1). - simpl. now simp irev_aux iapp. - simp irev_aux. destruct (eq_sym (add_succ_comm n (j + j2))). simpl. specialize (H _ acc2). rewrite H. clear H. refine (iapp_eq (n + S j, _) (S n + j, _) (_, _) (_, _) _ _); try constructor. clear Heq0. unshelve refine (DepElim.pack_sigma_eq _ _). exact (eq_sym Heq). reflexivity. Defined.
imports: Program Equations.Prop.EqDecInstances Equations.Prop.Equations