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