proposition: Lemma rev_aux_app_hetero_eq : 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. apply hetero_veq_refl. - simp irev_aux. destruct (eq_sym (add_succ_comm n (j + j2))). simpl. specialize (X _ acc2). simp iapp in X. eapply hetero_veq_trans. eapply X. apply (iapp_hetero_cong (n:=n + S j) (n' := S n + j)); auto with hetero_veq. apply hetero_veq_transport_right'. Qed.
imports: Program Equations.Prop.EqDecInstances Equations.Prop.Equations