(axiom obj *)
(axiom false *) ; not sure about this one
(axiom and (implies * * *))
(axiom or (implies * * *))
(axiom not (implies * *))
(axiom and_get (forall (a *) (b *) (implies (and a b) a)))
(axiom and_skip (forall (a *) (b *) (implies (and a b) b)))

(axiom to_clause_1 (forall (a *) (b *) (implies (implies a b) a (not b) false)))
(axiom to_clause_2 (forall (a *) (b *) (implies (implies a b) (not b) b false)))
(axiom absurd_n (forall (a *) (implies (implies (not a) false) a)))
(axiom absurd_p (forall (a *) (implies (implies a false) (not a))))
(axiom excl_mid_pn (forall (a *) (implies a (not a) false)))
(axiom excl_mid_np (forall (a *) (implies (not a) a false)))

(axiom unit_res_pn (forall (a *) (b *) (implies a (or (not a) b) b)))
(axiom unit_res_np (forall (a *) (b *) (implies (not a) (or a b) b)))

(axiom eq (forall (a *) (implies a a *)))
(axiom congr (forall 
  (t *) (s *) 
  (a (implies t s)) (a' (implies t s)) 
  (b t) (b' t) (implies (eq (implies t s) a a') (eq t b b') (eq s (a b) (a' b')))))

(axiom ex (forall (a *) (implies (implies a *) *)))
(axiom unskolem
 (forall (T *) (P (implies obj T *))
   (implies
     (exists (f (implies obj T)) (forall (y obj) (P y (f y))))
     (forall (y obj) (exists (x T) (P y x))))))

(lemma x42
  (fun (Q (implies obj *))
  (fun (H (exists (f (implies obj obj obj)) (forall (x obj) (y obj) (Q (f x y)))))
       (x obj)
       (unskolem obj (fun (_dummy obj) (x0 obj) (Q x0))
         (unskolem (implies obj obj)
           (fun (_dummy obj) (fx (implies obj obj)) (forall (y obj) (Q (fx y)))) H x)))))
quit

(axiom a *)
(lemma l1 (implies a *))

(axiom x0 a)
(axiom p (implies a *))
(axiom q *)
(lemma l2 (fun (z (forall (x a) (implies (p x) q))) (y (forall (x a) (p x)))
  (
   (z x0) 
   (y x0)
  ) 
  ))
  
quit

(lemma l1 (fun (a prop) (x a) x))
(lemma mp (fun (a prop) (b prop) (y a) (x (implies a b)) (x y)))
quit
(axiom a Prop)
(axiom b Prop)
(lemma mp (fun (y a) (x (implies a b)) (x y)))
quit