proposition: Lemma comp_eval : forall P ectx ectx' t t', computable P -> (forall v, TmEval ectx' t' v -> TmEval ectx t v) -> comp_term P ectx' t' -> comp_term P ectx t.
proof: Proof. intros. destruct H. destruct (comp_norm0 ectx' t' H1) as [v eval']. apply comp_term_of_val0 with (v := v); auto. eapply comp_val_of_term0; now eauto. Qed.
imports: List Arith Bool