proposition: Fact comap_uparam_forall `{Funext} A A' (PA : A <=> A') B B' (PB : forall a a', PA a a' -> B a <=> B' a') : comap (uparam_forall PA PB) = fun f a => comap (PB _ _ (map_in_R PA _ _ 1)) (f (map PA a)).
proof: Proof. reflexivity. Qed.
imports: elpi(elpi) Coq(ssreflect) HoTT(HoTT) HoTT_additions Hierarchy