Set: pp::colors
  Set: pp::unicode
  Assumed: A
  Assumed: B
  Assumed: f
  Defined: g
  Assumed: h
  Assumed: hinv
  Assumed: Inv
  Assumed: H1
  Proved: f_eq_g
  Proved: Inj
Definition g (A : Type) (f : A → A → A) (x y : A) : A := f y x
Theorem f_eq_g (A : Type) (f : A → A → A) (H1 : Π x y : A, (f x y) = (f y x)) : f = (g A f) :=
    Abst (λ x : A,
            Abst (λ y : A,
                    let L1 : (f x y) = (f y x) := H1 x y,
                        L2 : (f y x) = (g A f x y) := Refl (g A f x y)
                    in Trans L1 L2))
Theorem Inj (A B : Type)
    (h : A → B)
    (hinv : B → A)
    (Inv : Π x : A, (hinv (h x)) = x)
    (x y : A)
    (H : (h x) = (h y)) : x = y :=
    let L1 : (hinv (h x)) = (hinv (h y)) := Congr2 hinv H,
        L2 : (hinv (h x)) = x := Inv x,
        L3 : (hinv (h y)) = y := Inv y,
        L4 : x = (hinv (h x)) := Symm L2,
        L5 : x = (hinv (h y)) := Trans L4 L1
    in Trans L5 L3
10