как переписать что-то верное в True

Question

с учетом цели ... <-> Forall P [] Я хочу переписать Forall P [] в True, а затем переписать True / \ Forall P ys to Forall P ys

(1) существует теорема Forall_nil, говорящая Forall P [] но как я могу использовать это, чтобы переписать Forall P [] в True (2) не существует очевидных правил упрощения / переписывания, таких как True / \ P <-> P

Answer 1

Эквиваленты для их перезаписи отсутствуют в стандартной библиотеке, но их довольно легко доказать на месте.

Theorem forall_empty A (P : A -> Prop) : Forall P [] <-> True.
Proof. firstorder. Qed.

Theorem True_and (P : Prop) : True /\ P <-> P.
Proof. firstorder. Qed.