proposition: Lemma map_var_a : forall {n m o} f g a, @map_var n o (fun t => f (g t)) a = @map_var m o f (@map_var n m g a).
proof: Proof. depind a; autorewrite with map_var; auto. Qed.
imports: Program Equations(Equations) Coq.Classes.EquivDec Arith