proposition: Lemma L2 : forall c : chain, parametric c -> computation_length a (c A a) = computation_length b (c B b).
proof: Proof. intros c Hc;apply L; apply Hc; now red. Qed.
imports: Coq(Relations RelationClasses Lia List) Param(Param) additions(More_on_positive)