proposition: Lemma map_var_b : forall {n m} (f g : var n -> var m), (forall x, f x = g x) -> forall a, map_var f a = map_var g a.
proof: Proof. depind a; autorewrite with map_var; try f_equal; auto. Qed.
imports: Program Equations(Equations) Coq.Classes.EquivDec Arith