proposition: Lemma lift_type_by_id : forall {n} (t : type n) P, (forall x, lift_var_by P x = x) -> lift_type_by P t = t.
proof: Proof. depind t; intros; autorewrite with lift_type_by; rewrite ?H, ?IHt1, ?IHt2; auto. intros; depelim x; autorewrite with lift_var_by map_var; try f_equal; auto. Qed.
imports: Program Equations(Equations) Coq.Classes.EquivDec Arith