new tack beginning to work

down to just one goal:

  T0 := trivialTorsor ℤ : Torsor ℤ
  Y : Type
  y : Y
  l : y == y
  ============================
   ap pr1
     (proofirrGuidedHomotopy T0 (confun T0 y) (confun T0 l)
        (makeGuidedHomotopy2 (confun T0 y) (confun T0 l))
        (makeGuidedHomotopy2 (confun T0 y) (confun T0 l))) ==
   idpath y