proposition: Lemma eval_f_rew : forall k (f:GFormula k), eval_f f = match f in GFormula k' return rtyp k' with | TT tk => eTT tk | FF tk => eFF tk | A k a _ => ea k a | X p => ex p | @AND k e1 e2 => eAND k (eval_f e1) (eval_f e2) | @OR k e1 e2 => eOR k (eval_f e1) (eval_f e2) | @NOT k e => eNOT k (eval_f e) | @IMPL k f1 _ f2 => eIMPL k (eval_f f1) (eval_f f2) | @IFF k f1 f2 => eIFF k (eval_f f1) (eval_f f2) | EQ f1 f2 => (eval_f f1) = (eval_f f2) end.
proof: Proof. intros k f; destruct f ; reflexivity. Qed.
imports: List Refl Bool Relation_Definitions Setoid