Tabela táticas em Coq

	A -> B	forall x:T, A	and A B	False	~ A	or A B	A a1 = B b1	a = b
Hipótese	apply	apply	destruct	inversion	unfold, apply	destruct	inversion	rewrite
Objetivo	intros	intros	split		intros	left, right