#!/usr/bin/perl

sub f($) {
  my $a = shift;
  if ($a == 0) { return "a"; }
  else { return "(f " . f($a-1) . ")"; }
}

sub rules($) {
  my $a = shift;
  my $f = f($a);
  my $f1 = f($a - 1);
  my $a1 = $a - 1;

  print "(let cong$a (alli (\\ a (impi (= a (h a)) (\\ u (congf (mp (alle a cong$a1) u)))))))\n";
  print "(let okcong$a (pf (all (\\ a (imp (= a (h a)) (= $f1 $f))))))\n";
  print "(assert_eq okcong$a cong$a)\n";
  print "(let pf$a (impi (= a (g a)) (\\ u (trans (mp pf$a1 u) (mp (alle a cong$a) u)))))\n";
  print "(let okpf$a (pf (imp (= a (g a)) (= a $f))))\n";
  print "(assert_eq pf$a okpf$a)\n";
}
print "
(let cong2 (alli (\\ a (impi (= a (h a)) (\\ u (congf u))))))
(let cong2res (pf (all (\\ a (imp (= a (h a)) (= (f a) (f (f a))))))))
(assert_eq cong2 cong2res)
(let pf2 (impi (= a (g a)) (\\ u (trans u (mp (alle a cong2) u)))))
(let okpf2 (pf (imp (= a (g a)) (= a (f (f a))))))
(assert_eq pf2 okpf2)
";

for (my $i=3; $i<350; $i++) { rules($i) }