Framework for working on https://math.stackexchange.com/questions/2962525/derive-simple-logical-laws-in-a-structure-with-not-and-implies

gabriel_framework.lean

inductive fml
| atom (i : ℕ)
| imp (a b : fml)
| not (a : fml)

open fml

infixr ` →' `:50 := imp -- right associative
local notation ¬ := fml.not

inductive prf : fml → Type
| axk (p q) : prf (p →' q →' p)
| axs (p q r) : prf $ (p →' q →' r) →' (p →' q) →' (p →' r)
| axX (p q) : prf $ (¬q →' ¬p) →' p →' q
| mp (p q) : prf p → prf (p →' q) → prf q

open prf

lemma pqpp (p q : fml) : prf $ (p →' q) →' (p →' p) :=
begin
  apply mp (p →' q →' p) ((p →' q) →' p →' p) (axk p q),
  exact axs p q p
end

theorem p_implies_p (p : fml) : prf $ p →' p :=
begin
  exact mp (p →' p →' p) (p →' p) (axk p p) (pqpp p (p →' p)), 
end