fact: Definition htpy_ind_beta : htpy_ind f idhtpy = d := transport (fun p : (f;idhtpy) = (f;idhtpy) => transport (fun gh => Q gh.1 gh.2) p d = d) (@path2_contr _ _ _ _ (path_contr (f;idhtpy) (f;idhtpy)) (idpath _))^ (idpath _).
imports: HoTT.Basics HoTT.Types Metatheory.Core