proposition: Lemma F2C_correct (p:positive) (fc : Fchain) : Fchain_correct p fc -> chain_correct p (F2C fc).
proof: Proof. split;auto with chains; intros until M;intro x; unfold F2C; specialize (H _ _ _ _ M (@Return A)); unfold Fapply, C1; red; unfold chain_apply; rewrite computation_eval_rw; apply H; apply Return_proper. Qed.
imports: Coq(Inverse_Image Inclusion Wf_nat NArith Arith PArith Recdef Wf_nat Lexicographic_Product Lia) additions(Addition_Chains Compatibility More_on_positive Wf_transparent Dichotomy BinaryStrat) Coq(Lia)