proposition: Theorem get_imap : forall n (i : fin n) (ls : ilist A n), get (imap ls) i = f (get ls i).
proof: Proof. intros. funelim (imap ls). - depelim i. - depelim i. + repeat rewrite get_equation_2. reflexivity. + repeat rewrite get_equation_3. apply H. Qed.
imports: Arith List Program Equations.Prop.Equations