proposition: Lemma match_eq : forall A B : Type, forall x : A, forall (r : dynr) (b : bool) (P Q : typer r), result x b -> result x P -> result x Q -> result x (if b then P else Q).
proof: Proof. intros A B x r b P Q r1 r2 r3. elim r1; intros f1 b1. elim r2; intros f2 b2. elim r3; intros f3 b3. rewrite b1, b2, b3. exact (R (fun y=>if (f1 y) then (f2 y) else f3 y) (meq_refl _)). Defined.
imports: Mtac2(Base Logic Datatypes List)