proposition: Theorem fget_fimap : forall n (i : ffin n) (ls : filist A n), fget (fimap ls) i = f (fget ls i).
proof: Proof. intros. funelim (fimap ls); depelim i; now simp fget. Qed.
imports: Arith List Program Equations.Prop.Equations