ivy/test/theorem2.ivy

#lang ivy1.7

theorem impi = {
    function p : bool
    function q : bool
    {
        property p
        property q
    }
    property p -> q
}

theorem refl = {
    type t
    property X:t = X
}

relation a

type t1
var b : t1

object bar = {
    theorem silly = {
        property a -> (b = b)
    }
    proof apply impi; apply refl
}