proposition: Lemma convert_ilist_refl {A} (n : nat) (l : ilist A n) : convert_ilist eq_refl l = l.
proof: Proof. induction l. reflexivity. simpl. now rewrite IHl. Defined.
imports: Program Equations.Prop.EqDecInstances Equations.Prop.Equations