proposition: Lemma maponpaths_for_constant_function {T1 T2 : UU} (x : T2) {t1 t2 : T1} (e: t1 = t2): maponpaths (fun _: T1 => x) e = idpath x.
proof: Proof. induction e. apply idpath. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.Tactics