proposition: Lemma L : forall(gammaA : @computation A) (gammaB : @computation B), computation_R _ _ R_true gammaA gammaB -> @computation_length A a gammaA = @computation_length B b gammaB.
proof: Proof. induction 1. - reflexivity. - simpl; now rewrite (H a b). Qed.
imports: Coq(Relations RelationClasses Lia List) Param(Param) additions(More_on_positive)