fact: Fixpoint doTripletsR (L : list rZ) : rArray vM -> mbDT := fun Ar => match L with | nil => quatuor _ _ _ _ Ar false nil emptyTrace | a :: L1 => match doTripletFs (getT a) Ar with | quatuor Ar' true L' T' => quatuor _ _ _ _ Ar' true L' T' | quatuor Ar' _b' L' T' => match doTripletsR L1 Ar' with | quatuor Ar'' b'' L'' T'' => quatuor _ _ _ _ Ar'' b'' (appendRz L' L'') (appTrace T' T'') end end end.