tests/lean/autoPPExplicit.lean - third_party/github.com/leanprover/lean4 - Git at Google


            
            def f {a b c : α} : a = c :=

            
              Eq.trans (a := a) (b := b = c)