postulate Human_Being:: Set
postulate john:: Human_Being
postulate mary:: Human_Being
postulate Is_Student :: Human_Being -> Set
postulate mary_is_student:: Is_Student mary
Lemma1 :: Set
       = Is_Student john -> Is_Student mary
proof_lemma1 :: Lemma1
             = \(x:: Is_Student john) -> mary_is_student

Lemma2 :: Set
       = Is_Student mary -> Is_Student john


proof_lemma2 :: Lemma2
             = \(x:: Is_Student mary) -> {!!}