proposition: Lemma hold_eIMPL : forall k e1 e2, hold k (eIMPL k e1 e2) <-> (hold k e1 -> hold k e2).
proof: Proof. intros k; destruct k ; simpl. - intros. apply iff_refl. - intros e1 e2. unfold is_true. destruct e1,e2 ; simpl ; intuition congruence. Qed.
imports: List Refl Bool Relation_Definitions Setoid