proposition: Lemma eval_f_morph : forall (ev ev' : forall (k: kind), TA -> rtyp k), (forall k a, eiff k (ev k a) (ev' k a)) -> forall (k: kind)(f : GFormula k), (eiff k (eval_f ev f) (eval_f ev' f)).
proof: Proof. intros ev ev' H k f; induction f as [| | | |? ? IHf1 ? IHf2|? ? IHf1 ? IHf2|? ? IHf |? ? IHf1 ? ? IHf2|? ? IHf1 ? IHf2|]; simpl. - reflexivity. - reflexivity. - reflexivity. - apply H. - rewrite IHf1. rewrite IHf2. reflexivity. - rewrite IHf1. rewrite IHf2. reflexivity. - rewrite IHf. reflexivity. - rewrite IHf1. rewrite IHf2. reflexivity. - rewrite IHf1. rewrite IHf2. reflexivity. - simpl in *. intuition congruence. Qed.
imports: List Refl Bool Relation_Definitions Setoid