proposition: Theorem if_flip_helper {B: Type} {b: bool} (C E: true = b -> B) (D F: false = b -> B): (forall (r: true = b), C r = E r) -> (forall (r: false = b), D r = F r) -> (if b as an return an = b -> B then C else D) eq_refl = (if b as an return an = b -> B then E else F) eq_refl.
proof: Proof. intros. destruct b. apply H. apply H0. Qed.
imports: Arith Coq.Classes.DecidableClass Coq.Program.Wf List Lia PeanoNat Program Equations(Equations)