∀ n, leibniz (invert_permut_body (n+1)) (λf. λm. if (m = (f (n+1))) then (n+1) else (invert_permut n f m))

Theorem eq_invert_permut_body_S : forall (n:nat.nat), leibniz.leibniz ((nat.nat -> nat.nat) -> nat.nat -> nat.nat) (invert_permut_body (nat.S n)) (fun (f:(nat.nat -> nat.nat)) => fun (m:nat.nat) => bool.match_bool_type (nat.nat) (nat.S n) (invert_permut n f m) (nat.eqb m (f (nat.S n)))).

theorem eq_invert_permut_body_S : \forall (n:nat). (leibniz) ((nat -> nat) -> nat -> nat) ((invert_permut_body) ((S) n)) (\lambda f : nat -> nat. \lambda m : nat. (match_bool_type) (nat) ((S) n) ((invert_permut) n f m) ((eqb) m (f ((S) n)))).

theorem eq_invert_permut_body_S : forall (n:nat.nat) , (((leibniz.leibniz) (((nat.nat) -> nat.nat) -> (nat.nat) -> nat.nat)) (((permutation.invert_permut_body) ) (((nat.S) ) (n)))) (fun (f : (nat.nat) -> nat.nat) , fun (m : nat.nat) , ((((bool.match_bool_type) (nat.nat)) (((nat.S) ) (n))) (((((permutation.invert_permut) ) (n)) (f)) (m))) ((((nat.eqb) ) (m)) ((f) (((nat.S) ) (n))))).

eq_invert_permut_body_S : LEMMA (FORALL(n:nat_sttfa_th.sttfa_nat):leibniz_sttfa_th.leibniz[[[nat_sttfa_th.sttfa_nat -> nat_sttfa_th.sttfa_nat] -> [nat_sttfa_th.sttfa_nat -> nat_sttfa_th.sttfa_nat]]](permutation_sttfa.invert_permut_body(nat_sttfa_th.sttfa_S(n)))((LAMBDA(f:[nat_sttfa_th.sttfa_nat -> nat_sttfa_th.sttfa_nat]):(LAMBDA(m:nat_sttfa_th.sttfa_nat):bool_sttfa_th.match_bool_type[nat_sttfa_th.sttfa_nat](nat_sttfa_th.sttfa_S(n))(permutation_sttfa.invert_permut(n)(f)(m))(nat_sttfa_th.eqb(m)(f(nat_sttfa_th.sttfa_S(n))))))))

Printing for OpenTheory is not working at the moment.