proposition: Lemma refine_match_nat {A} {P : nat -> nat -> Prop} {Q : forall n, (forall n', P n' n -> A) -> Prop} : forall (cO : Comp A) cS n cO' cS' (y : forall n', P n' n -> A), (refine cO (ret cO')) -> (forall n (y : forall n', P n' (S n) -> A), Q (S n) y -> refine (cS n) (ret (cS' n y))) -> Q n y -> refine (match n with | 0 => cO | S n' => cS n' end) (ret (match n return (forall n', P n' n -> A) -> A with | 0 => fun _ => cO' | S n' => fun y => cS' n' y end y)).
proof: Proof. destruct n; eauto. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Sets.Ensembles Coq.ZArith.ZArith Coq.Classes.Morphisms Coq.Classes.SetoidTactics Fiat.Computation Fiat.Computation.SetoidMorphisms Coq.Logic.FunctionalExtensionality