proposition: Lemma makeTripletsFunIncl : forall (e : rExpr) (l l' : list triplet) (n n' : rNat) (s' : rZ), makeTripletsFun l n e = tRC l' s' n' -> incl l l'.
proof: Proof. RecExpr. auto with datatypes stalmarck. lapply (H' l l' n r1 r0); auto with stalmarck. rewrite <- H0; auto with stalmarck. lapply (H' l l0 n r3 r2); [ intros H'9 | idtac ]; auto with stalmarck. lapply (A l0 l2 r3 r5 r4); [ intros H'10 | idtac ]; auto with stalmarck. apply incl_tran with l0; auto with stalmarck. apply incl_tran with l2; auto with datatypes stalmarck. Qed.