(p ^ q) -> k

Stream: general

[Cameron]

Sorry last question. I have a show _ from _ and i get the error that i am expecting something of type k but i have something of type p ^ q -> k, how can i isolate just the right side of the implication? when i assume p is true and q is true before the show command i still run into issues

[Mario Carneiro]

you can use assume hpq : p /\ q,

[Mario Carneiro]

that contains a proof of the conjunction, which you can destruct with hpq.left and hpq.right

[Chris Hughes]

I think you might actually need hk ⟨hp, hq⟩ where hk is your proof of p ^ q -> k and hp is your proof of p and hq is your proof of q