proposition: Lemma convert_ilist_trans : forall {A : Set} {n m o : nat} (p : n = m) (r : m = o) (l : ilist A n), convert_ilist r (convert_ilist p l) = convert_ilist (eq_trans p r) l.
proof: Proof. intros. simplify_eqs. now rewrite !convert_ilist_refl. Qed.
imports: Program Equations.Prop.EqDecInstances Equations.Prop.Equations